.. nb:name: cs1
.. nb:database: cs1

Case Study: Intelligence Agency
===============================

This case study largely extends the scenario of the paper that first
presented ProvSQL :cite:`DBLP:journals/pvldb/SenellartJMR18`. Through a
security-classification scenario, it demonstrates custom semirings,
clearance levels under negation, where-provenance, probability computation with several algorithms, and
circuit export.

The Scenario
------------

An intelligence agency maintains a database of seven employees spread
across three cities. Each employee's record is classified at a level
ranging from *unclassified* to *top secret*: the clearance an analyst needs
to know that the employee exists. Your tasks:

* identify which cities are served by more than one agent,
* determine the minimum clearance level needed to infer each result,
* find cities with exactly one agent (sensitive: whatever is traced back
  to that city's station points to the one agent there),
* track where in the database each output value originated,
* compute the probability that a city remains a single-agent post
  after accounting for possible-world uncertainty,
* find at which clearance levels an analyst would wrongly conclude
  that a city has a single agent, and which allied services would.


Setup
-----

.. nb:skip
.. tip::

   **Prefer not to install? Use the Playground.** You can skip the manual
   setup below: open this case study `as a runnable notebook in the ProvSQL
   Playground <https://provsql.org/playground/?nb=cs1>`_ (every query is a
   cell, and the opening cells set up the database for you), or open the bare
   `cs1 database <https://provsql.org/playground/?db=cs1>`_ and run the queries
   as you read. The Playground bundles no external tools, so the steps that
   call an external knowledge compiler (``d4``, ``c2d``…) or the ``graph-easy``
   ASCII renderer (:sqlfunc:`view_circuit`) detect its absence and report it
   instead of returning a result -- the cells still run cleanly; the default
   probability evaluation works throughout (it chooses among the built-in
   exact methods), as does everything else. See the
   :ref:`Playground note <playground-note>`.

.. nb:omit-begin

This case study assumes a working ProvSQL installation (see
:doc:`getting-provsql`). Download :download:`setup.sql <../../casestudy1/setup.sql>`
and load it into a fresh PostgreSQL database:

.. code-block:: bash

    psql -d mydb -f setup.sql

The setup script calls :sqlfunc:`setup_search_path`, which adds
``provsql`` to the database's ``search_path``: every new session calls
ProvSQL's functions without the ``provsql.`` prefix.

.. nb:omit-end

.. nb:setup: ../../casestudy1/setup.sql

This creates:

* ``classification_level`` -- an ordered ENUM
  (``unclassified`` < ``restricted`` < ``confidential`` < ``secret`` < ``top_secret`` < ``unavailable``)
  where ``unavailable`` is a sentinel representing the semiring 𝟘 (no derivation possible)
* ``personnel`` -- 7 agents with name, position, city, and the
  classification level of their record


Step 1: Explore the Database
-----------------------------

Inspect the ``personnel`` table:

.. code-block:: postgresql

    SELECT * FROM personnel ORDER BY id;

You should see seven rows: Juma (Director, Nairobi), Paul (Janitor, Nairobi),
David (Analyst, Paris), Ellen (Field agent, Beijing), Aaheli (Double agent,
Paris), Nancy (HR, Paris), and Jing (Analyst, Beijing).


Step 2: Enable Provenance and Create a Name Mapping
----------------------------------------------------

Enable provenance tracking on ``personnel`` and create a mapping so that
provenance tokens can be labelled with agent names:

.. code-block:: postgresql

    SELECT add_provenance('personnel');
    DROP TABLE IF EXISTS personnel_name;
    SELECT create_provenance_mapping('personnel_name', 'personnel', 'name');

After :sqlfunc:`add_provenance`, every row of ``personnel`` has a unique UUID
token in its ``provsql`` column. The mapping ``personnel_name``
associates each token with the corresponding agent's name.


Step 3: Cities Shared by Multiple Agents
-----------------------------------------

Which cities have at least two agents? Use a self-join with an ``id``
inequality to generate all unordered pairs, then apply
:sqlfunc:`sr_formula` to see which agents contribute to each city:

.. code-block:: postgresql

    SELECT p1.city,
           sr_formula(provenance(), 'personnel_name') AS formula
    FROM personnel p1
    JOIN personnel p2 ON p1.city = p2.city AND p1.id < p2.id
    GROUP BY p1.city
    ORDER BY p1.city;

The formula for Nairobi is ``Juma ⊗ Paul``: both agents must be present
for Nairobi to appear. Beijing similarly shows ``Ellen ⊗ Jing``. Paris,
with three agents, shows all three pairwise products joined by ``⊕``.


Step 4: Minimum Security Clearance (sr_minmax)
-----------------------------------------------

For each shared city, what is the *minimum clearance level* required to
have inferred that the city has multiple agents? The analyst must see
both agents of some pair in the city.

The min-max m-semiring, available as :sqlfunc:`sr_minmax`, answers this
over the ``classification_level`` enum:

* ``⊕`` (OR combination) = ``min``: to infer *either* agent was
  involved, you only need clearance for the less-classified one (one
  witness suffices to establish the disjunction).
* ``⊗`` (AND/join) = ``max``: to confirm *both* agents are present,
  you need clearance for the more-classified one (you must be able to
  access both records to establish the join).

The third argument gives the carrier enum: only its type is used, so it is
written ``NULL::classification_level``:

.. code-block:: postgresql

    DROP TABLE IF EXISTS personnel_level;
    SELECT create_provenance_mapping('personnel_level',
                                     'personnel', 'classification');

    SELECT p1.city,
           sr_minmax(provenance(), 'personnel_level',
                     NULL::classification_level) AS min_clearance
    FROM personnel p1
    JOIN personnel p2 ON p1.city = p2.city AND p1.id < p2.id
    GROUP BY p1.city
    ORDER BY p1.city;

Results: Nairobi requires ``restricted`` (Paul is the more-classified of
the two agents, and both must be accessed to confirm the pair). Beijing
requires ``secret`` (Ellen and Jing are both classified ``secret``). Paris
requires ``confidential``: the more-classified of David and Nancy is
``confidential``, the lowest such maximum among all Paris pairs, so
``confidential`` clearance suffices to confirm at least one pair.


Step 5: Cities with Exactly One Agent (EXCEPT / Monus)
-------------------------------------------------------

A city with a single agent is sensitive: whatever is traced back to the
agency's station there (a report, an expense, a contact) points to one
person, where with two agents or more it could be any of them. Find the
cities with exactly one agent, as the cities with an agent minus those
with at least two, using ``EXCEPT``:

.. code-block:: postgresql

    SELECT city,
           sr_formula(provenance(), 'personnel_name') AS formula
    FROM (
        SELECT DISTINCT city FROM personnel
      EXCEPT
        SELECT p1.city
        FROM personnel p1
        JOIN personnel p2 ON p1.city = p2.city AND p1.id < p2.id
        GROUP BY p1.city
    ) t
    ORDER BY city;

.. note::

   ProvSQL evaluates ``EXCEPT`` with the *monus* operator ``⊖`` of the
   provenance semiring. Every city
   appears in the result with a provenance formula. Whether that formula
   evaluates to ``𝟘`` depends on the semiring it is evaluated in and on
   the values given to the agents, not on the formula alone: with
   polynomials over the agents' names, no city's formula is ``𝟘``;
   with every agent present (true, in the Booleans), all three
   cities are; in the min-max semiring of security levels, only
   Beijing's is. Nairobi's formula
   ``(Juma ⊕ Paul) ⊖ (Juma ⊗ Paul)`` reads: "at least one of Juma
   or Paul is present, minus the event where both are."


Step 6: Where-Provenance
-------------------------

Where-provenance tracks *which column of which input row* produced each
output value. Enable it and re-run the shared-city query:

.. code-block:: postgresql

    SET provsql.provenance = 'where';

    SELECT p1.city,
           where_provenance(provenance()) AS source
    FROM personnel p1
    JOIN personnel p2 ON p1.city = p2.city AND p1.id < p2.id
    GROUP BY p1.city
    ORDER BY p1.city;

    SET provsql.provenance = 'semiring';

Each city output value is traced back to the ``city`` column (column 4)
of the ``personnel`` table for every agent in that city. The notation
``[personnel:〈token〉:4;...]`` shows the token and column index of each
contributing row; the trailing ``[]`` is the untracked ``source``
column itself.

Seeing it in Studio: Where mode
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

:ref:`ProvSQL Studio's Where mode <studio-where-mode>` shows the same
answer interactively. Pick :guilabel:`Where` from the mode switcher at the
top and run the shared-city query without the two ``SET`` statements and
without the ``source`` column: Where mode sets ``provsql.provenance``
itself. Then hover a city in the result: the ``city`` cells of every agent
in that city light up in the ``personnel`` table of the
:guilabel:`Provenance-Tagged Relations` panel, both agents for Nairobi and
all three for Paris. To return to the notebook, if you are following one,
pick :guilabel:`Notebook` from the same switcher.


Step 7: Assign Probabilities
-----------------------------

Suppose the existence of each agent in the database is uncertain.
Assign each agent a probability equal to ``id / 10.0``:

.. code-block:: postgresql

    SELECT set_prob(provenance(), id / 10.0) FROM personnel;

Now Juma has probability 0.1, Paul 0.2, and so on up to Jing 0.7.


Step 8: Probability -- Exact
----------------------------

Compute the exact probability that each city is a single-agent city:

.. code-block:: postgresql

    SELECT city,
           ROUND(probability_evaluate(provenance())::numeric, 4) AS prob
    FROM (
        SELECT DISTINCT city FROM personnel
      EXCEPT
        SELECT p1.city
        FROM personnel p1
        JOIN personnel p2 ON p1.city = p2.city AND p1.id < p2.id
        GROUP BY p1.city
    ) t
    ORDER BY city;

Nairobi (agents with probabilities 0.1 and 0.2) has probability
``0.1 × 0.8 + 0.9 × 0.2 = 0.26`` of having exactly one agent. Beijing
(0.4 and 0.7) scores ``0.54``. Paris (0.3, 0.5, 0.6) gives ``0.41``.


Step 9: Probability -- Monte Carlo
-----------------------------------

For larger circuits, exact evaluation can be expensive. Monte Carlo
sampling gives an approximate answer:

.. code-block:: postgresql

    SELECT city,
           probability_evaluate(
               provenance(), 'monte-carlo', '10000') AS prob
    FROM (
        SELECT DISTINCT city FROM personnel
      EXCEPT
        SELECT p1.city
        FROM personnel p1
        JOIN personnel p2 ON p1.city = p2.city AND p1.id < p2.id
        GROUP BY p1.city
    ) t
    ORDER BY city;

With 10 000 samples the result is accurate to roughly ±0.01
(see `Margin of error <https://en.wikipedia.org/wiki/Margin_of_error>`_).
Results will vary slightly between runs due to sampling.
Compare the runtime against the exact method (``\timing`` in psql,
or the per-query timing Studio displays).


Step 10: Probability -- Knowledge Compiler
------------------------------------------

.. note::

   This step uses an external knowledge compiler such as ``d4`` or
   ``dsharp``, which must be on your ``PATH`` (or in a directory
   listed in the ``provsql.tool_search_path`` GUC, see
   :doc:`the configuration chapter <configuration>`). The query below
   guards the call with :sqlfunc:`tool_available`, so where no such
   compiler is installed -- in particular in the
   :ref:`Playground <playground-note>`, which bundles none -- it reports
   that instead of failing, and you can read on.

A knowledge compiler converts the provenance circuit to a *d-DNNF*
representation, which enables efficient exact probability evaluation
on large circuits of specific forms:

.. code-block:: postgresql

    SELECT city,
           CASE WHEN tool_available('d4')
                THEN ROUND(probability_evaluate(
                         provenance(), 'compilation', 'd4')::numeric, 4)::text
                ELSE '(needs external compiler d4; unavailable here)'
           END AS prob
    FROM (
        SELECT DISTINCT city FROM personnel
      EXCEPT
        SELECT p1.city
        FROM personnel p1
        JOIN personnel p2 ON p1.city = p2.city AND p1.id < p2.id
        GROUP BY p1.city
    ) t
    ORDER BY city;

Compare the runtime (``\timing`` in psql, or Studio's per-query
timing) against the possible-worlds and Monte Carlo methods. On this
small example the external knowledge compiler is slower: invoking an
external process carries an overhead that only pays off on much larger
circuits.


Step 11: Visualise a Provenance Circuit
-----------------------------------------

:sqlfunc:`view_circuit` renders the provenance circuit as an ASCII
box-art diagram using
`graph-easy <https://metacpan.org/dist/Graph-Easy>`_
(which must be on your ``PATH``). The query guards the call with
:sqlfunc:`tool_available`, so without ``graph-easy`` -- in particular in
the :ref:`Playground <playground-note>`, where Studio's interactive
:doc:`Circuit mode <studio>` is the better view anyway -- it returns a
message instead of failing:

.. code-block:: postgresql

    SELECT city,
           CASE WHEN tool_available('graph-easy')
                THEN view_circuit(provenance(), 'personnel_name')
                ELSE '(needs the graph-easy renderer; use Studio Circuit mode)'
           END AS circuit
    FROM (
        SELECT DISTINCT city FROM personnel
      EXCEPT
        SELECT p1.city
        FROM personnel p1
        JOIN personnel p2 ON p1.city = p2.city AND p1.id < p2.id
        GROUP BY p1.city
    ) t
    WHERE city = 'Nairobi';

The result shows the monus gate at the top, with ``Juma`` and
``Paul`` as leaf inputs, rendered in box-art notation in the terminal.


Step 12: Export to XML
-----------------------

:sqlfunc:`to_provxml` serialises the provenance circuit to
`PROV-XML <https://www.w3.org/TR/prov-xml/>`_, the W3C standard for
provenance interchange, which can be processed by any standard XML tool:

.. code-block:: postgresql

    SELECT city,
           to_provxml(provenance(), 'personnel_name') AS provxml
    FROM (
        SELECT DISTINCT city FROM personnel
      EXCEPT
        SELECT p1.city
        FROM personnel p1
        JOIN personnel p2 ON p1.city = p2.city AND p1.id < p2.id
        GROUP BY p1.city
    ) t
    WHERE city = 'Nairobi';


Step 13: Large Circuit Benchmark
----------------------------------

To compare the three probability algorithms at scale, create a synthetic
100 × 100 random-probability matrix and enable provenance tracking on it:

.. code-block:: postgresql

    DROP TABLE IF EXISTS matrix CASCADE;
    CREATE TABLE matrix AS
    SELECT ones.n + 10 * tens.n AS x,
           other.n + 10 * tens2.n AS y,
           random() AS prob
    FROM (VALUES(0),(1),(2),(3),(4),(5),(6),(7),(8),(9)) ones(n),
         (VALUES(0),(1),(2),(3),(4),(5),(6),(7),(8),(9)) tens(n),
         (VALUES(0),(1),(2),(3),(4),(5),(6),(7),(8),(9)) other(n),
         (VALUES(0),(1),(2),(3),(4),(5),(6),(7),(8),(9)) tens2(n);

    SELECT add_provenance('matrix');
    SELECT set_prob(provenance(), prob) FROM matrix;

The last query returns one (empty) row per cell of the matrix, 10,000 in
all.

Now run the same path query with each method in turn, timing each
(``\timing`` in psql, or Studio's per-query timing):

.. code-block:: postgresql

    -- No method named: the exact probability, by the method expected to
    -- be cheapest on each row's circuit
    SET provsql.last_eval_method = '';
    SELECT m1.x, m2.y,
           probability_evaluate(provenance()) AS prob
    FROM matrix m1, matrix m2
    WHERE m2.x = m1.y AND m1.x > 90 AND m2.x > 90 AND m2.y > 90
    GROUP BY m1.x, m2.y
    ORDER BY m1.x, m2.y;

    SHOW provsql.last_eval_method;

.. code-block:: postgresql

    -- Exact enumeration over all possible worlds
    SELECT m1.x, m2.y,
           probability_evaluate(provenance(), 'possible-worlds') AS prob
    FROM matrix m1, matrix m2
    WHERE m2.x = m1.y AND m1.x > 90 AND m2.x > 90 AND m2.y > 90
    GROUP BY m1.x, m2.y
    ORDER BY m1.x, m2.y;

.. code-block:: postgresql

    -- Monte Carlo sampling (9604 samples ≈ 1 % error at 95 % confidence)
    SELECT m1.x, m2.y,
           probability_evaluate(provenance(), 'monte-carlo', '9604') AS prob
    FROM matrix m1, matrix m2
    WHERE m2.x = m1.y AND m1.x > 90 AND m2.x > 90 AND m2.y > 90
    GROUP BY m1.x, m2.y
    ORDER BY m1.x, m2.y;

.. code-block:: postgresql

    -- Tree-decomposition-based exact compilation (built-in, no external tool)
    SELECT m1.x, m2.y,
           probability_evaluate(provenance(), 'tree-decomposition') AS prob
    FROM matrix m1, matrix m2
    WHERE m2.x = m1.y AND m1.x > 90 AND m2.x > 90 AND m2.y > 90
    GROUP BY m1.x, m2.y
    ORDER BY m1.x, m2.y;

.. code-block:: postgresql

    -- Knowledge compilation via external tool d4 (guarded with
    -- tool_available, so it reports rather than fails where d4 is
    -- absent, e.g. in the Playground)
    SELECT m1.x, m2.y,
           CASE WHEN tool_available('d4')
                THEN probability_evaluate(provenance(), 'compilation', 'd4')::text
                ELSE '(d4 unavailable here)'
           END AS prob
    FROM matrix m1, matrix m2
    WHERE m2.x = m1.y AND m1.x > 90 AND m2.x > 90 AND m2.y > 90
    GROUP BY m1.x, m2.y
    ORDER BY m1.x, m2.y;

With no method named, :sqlfunc:`probability_evaluate` returns the exact
probability, and a cost-based chooser picks, for each circuit, the exact
method it expects to be cheapest (see :ref:`probability-guarantees`).
:ref:`provsql.last_eval_method <provsql-last-eval-method>` lists the
methods used since it was last cleared, so the query is preceded by
emptying it: here typically ``independent`` for some rows and ``d-tree``
for others, since the rows' circuits differ in shape. Studio
reports the method in its evaluation strip.

The Monte Carlo query uses ``9604`` samples, which gives roughly 1 %
additive error with 95 % confidence (by the formula
:math:`n = z^2 / (4\varepsilon^2)` with :math:`z = 1.96`,
:math:`\varepsilon = 0.01`;
see `Margin of error <https://en.wikipedia.org/wiki/Margin_of_error>`_).

The ``'tree-decomposition'`` method is exact and built into ProvSQL (no
external binary required). It is often the fastest exact method on simple
queries, but it fails on circuits with high treewidth; then fall back to
``'compilation'`` or one of the other methods.

``'independent'`` is the cheapest method of all -- it multiplies and adds
marginal probabilities directly -- but it applies only when the lineage is
*independent*, with no input tuple shared between the branches of an
:math:`\oplus` or :math:`\otimes`. The path query above is **not**
independent (the self-join ``m2.x = m1.y`` makes the two matrix lookups
share tuples), so ``probability_evaluate(provenance(), 'independent')``
raises ``ProvSQL: Not an independent circuit`` instead of returning a wrong
answer. Use it on tuple-independent lineage.


Step 14: The Boolean Expression Behind a Token
------------------------------------------------

:sqlfunc:`sr_boolexpr` returns the abstract Boolean formula of a provenance
circuit. Without a mapping it uses internal variable names ``x0``,
``x1``…; with an optional second argument naming a provenance
mapping table the leaves are labelled by the mapping's ``value``
column instead.

.. code-block:: postgresql

    SELECT city, sr_boolexpr(provenance()) AS boolexpr
    FROM (
        SELECT DISTINCT city FROM personnel
      EXCEPT
        SELECT p1.city
        FROM personnel p1
        JOIN personnel p2 ON p1.city = p2.city AND p1.id < p2.id
        GROUP BY p1.city
    ) t
    WHERE city = 'Nairobi';

For Nairobi, the result is the circuit ``(Juma ⊕ Paul) ⊖ (Juma ⊗ Paul)``
from Step 5 read as a Boolean function (``⊕`` as ``∨``, ``⊗`` as ``∧``,
``⊖`` as ``∧¬``) and rendered as a formula over anonymous variables.
Unlike with :sqlfunc:`sr_formula`, the provenance mapping is optional.


Step 15: Programmatic Circuit Inspection
------------------------------------------

What :sqlfunc:`view_circuit` renders, you can also walk programmatically
with the low-level circuit API. Capture Nairobi's monus token first:

.. code-block:: postgresql

    CREATE TEMP TABLE nairobi_token AS
    SELECT provenance() AS prov
    FROM (
        SELECT DISTINCT city FROM personnel
      EXCEPT
        SELECT p1.city
        FROM personnel p1
        JOIN personnel p2 ON p1.city = p2.city AND p1.id < p2.id
        GROUP BY p1.city
    ) t
    WHERE city = 'Nairobi';

:sqlfunc:`get_nb_gates` reports how many gates the current database's
provenance circuit holds:

.. code-block:: postgresql

    SELECT get_nb_gates();

:sqlfunc:`get_gate_type` and :sqlfunc:`get_children` give a single-step view
of the gate structure: they return the operator and direct children of a
gate.

.. code-block:: postgresql

    SELECT get_gate_type(prov)            AS root_type,
           get_children(prov)             AS root_children
    FROM nairobi_token;

For Nairobi, the root is a ``monus`` gate with two children: the ⊕
sub-circuit (``Juma ⊕ Paul``) and the ⊗ sub-circuit (``Juma ⊗ Paul``).
Recurse to inspect the children:

.. code-block:: postgresql

    SELECT (get_children(prov))[1]                        AS plus_token,
           get_gate_type((get_children(prov))[1])         AS plus_type,
           get_children((get_children(prov))[1])          AS plus_children
    FROM nairobi_token;

The leaves of the circuit are input gates that originate from the
``personnel`` table. :sqlfunc:`identify_token` performs a reverse lookup,
returning the table and column count for an input token:

.. code-block:: postgresql

    SELECT identify_token(child) AS source
    FROM nairobi_token, unnest(get_children((get_children(prov))[1])) AS child;

Both leaves resolve to ``(personnel, 5)``: the ``personnel`` table with
its five non-provenance columns (``id``, ``name``, ``position``, ``city``
and ``classification``).


Step 16: Revising a Probability
-------------------------------

New intelligence says Juma is almost certainly a real agent: his
probability should be 0.9, not 0.1. A probability is written once:
:sqlfunc:`set_prob` refuses a different value for a token that already has
one, and its error message points to :sqlfunc:`replace_input`, which gives
the row a fresh input gate with the new probability:

.. code-block:: postgresql

    UPDATE personnel SET provsql = replace_input(provsql, 0.9)
    WHERE name = 'Juma';

Queries from now on see the new value. Rerunning the query of Step 8,
Nairobi's single-agent probability becomes
``0.9 × 0.8 + 0.1 × 0.2 = 0.74``, and the other cities are unchanged:

.. code-block:: postgresql

    SELECT city,
           ROUND(probability_evaluate(provenance())::numeric, 4) AS prob
    FROM (
        SELECT DISTINCT city FROM personnel
      EXCEPT
        SELECT p1.city
        FROM personnel p1
        JOIN personnel p2 ON p1.city = p2.city AND p1.id < p2.id
        GROUP BY p1.city
    ) t
    ORDER BY city;

A result computed before the change keeps the old probability: the token
saved in Step 15 was built from Juma's old input gate, which is still in
the circuit, and it still evaluates to ``0.26``:

.. code-block:: postgresql

    SELECT ROUND(probability_evaluate(prov)::numeric, 4) AS prob
    FROM nairobi_token;


Step 17: Clearance Levels of a Negation
---------------------------------------

An analyst runs the query of Step 5 seeing only the agents whose records
are classified at or below the analyst's clearance. At which levels does
a city look single-agent?
:sqlfunc:`sr_minmax` (Step 4) cannot answer this for a query with
``EXCEPT``: it returns a single level, read as "from that level up", but
an analyst with more clearance sees more agents and may no longer see
the city as single-agent. :sqlfunc:`sr_clearance` returns the set of
levels at which the query returns the row, with negation read exactly.
Juma's row has a new token since Step 16, so the mapping is rebuilt
first:

.. code-block:: postgresql

    DROP TABLE IF EXISTS personnel_level;
    SELECT create_provenance_mapping('personnel_level',
                                     'personnel', 'classification');

    SELECT city,
           sr_clearance(provenance(), 'personnel_level',
                        NULL::classification_level) AS levels,
           visible_at(provenance(), 'personnel_level', 'unclassified')
             AS at_unclassified,
           (clearance_settling(provenance(), 'personnel_level',
                               NULL::classification_level)).*
    FROM (
        SELECT DISTINCT city FROM personnel
      EXCEPT
        SELECT p1.city
        FROM personnel p1
        JOIN personnel p2 ON p1.city = p2.city AND p1.id < p2.id
        GROUP BY p1.city
    ) t
    ORDER BY city;

Nairobi looks single-agent only at ``unclassified``, where Paul is
hidden, and Paris only at ``restricted``, where Nancy is the one agent
visible; Beijing never does. :sqlfunc:`sr_minmax` would answer
``unclassified`` and ``restricted``, suggesting every higher level too.
:sqlfunc:`visible_at` tests a single level, given as text, and
:sqlfunc:`clearance_settling` gives the level from which the answer no
longer changes (``restricted`` for Nairobi, ``confidential`` for Paris)
and that answer at the top level.


Step 18: What Allied Services Conclude
--------------------------------------

The agency shares some personnel files with allied services. Each ally
sees some of the agents, and unlike clearance levels, the allies are not
ordered. Record, for each agent, the allies the file is shared with, in a
new column whose type is an array over an enum of the allies:

.. code-block:: postgresql

    DROP TABLE IF EXISTS personnel_shared;
    ALTER TABLE personnel DROP COLUMN IF EXISTS shared_with;
    DROP TYPE IF EXISTS ally;
    CREATE TYPE ally AS ENUM ('bnd', 'dgse', 'mi6');
    ALTER TABLE personnel ADD COLUMN shared_with ally[];
    UPDATE personnel
    SET shared_with = CASE name WHEN 'Juma'   THEN '{mi6,dgse}'
                                WHEN 'Paul'   THEN '{mi6}'
                                WHEN 'David'  THEN '{dgse,bnd}'
                                WHEN 'Ellen'  THEN '{bnd}'
                                WHEN 'Aaheli' THEN '{}'
                                WHEN 'Nancy'  THEN '{mi6,dgse,bnd}'
                                WHEN 'Jing'   THEN '{dgse}' END::ally[];

    SELECT name, city, shared_with FROM personnel ORDER BY id;

How many agents does each ally see in each city? :sqlfunc:`sr_subset` reads
the labels of an enum as worlds, here one per ally, through a mapping that
gives the allies of each row; it returns the set of allies whose view
returns the result row. Build the mapping from the new column:

.. code-block:: postgresql

    SELECT create_provenance_mapping('personnel_shared',
                                     'personnel', 'shared_with');

Grouping the cities by their number of agents gives one row per number a
city can show, and :sqlfunc:`sr_subset` the allies to which it shows that
number:

.. code-block:: postgresql

    SELECT city, n AS agents,
           sr_subset(provenance(), 'personnel_shared', NULL::ally) AS allies
    FROM (SELECT city, count(*) AS n FROM personnel GROUP BY city) t
    GROUP BY city, n
    ORDER BY city, agents DESC;

No ally sees all of Paris: the BND and the DGSE see two of its agents, MI6
only Nancy. Paris thus looks single-agent to MI6, Nairobi to the DGSE, and
Beijing to both the BND and the DGSE.