Case Study: Intelligence Agency

This case study largely extends the scenario of the paper that first presented ProvSQL [Senellart et al., 2018]. 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

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 (every query is a cell, and the opening cells set up the database for you), or open the bare cs1 database 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 (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 Playground note.

This case study assumes a working ProvSQL installation (see Getting ProvSQL). Download setup.sql and load it into a fresh PostgreSQL database:

psql -d mydb -f setup.sql

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

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:

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:

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

After 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 sr_formula to see which agents contribute to each city:

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 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:

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:

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:

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

ProvSQL Studio’s Where mode shows the same answer interactively. Pick 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 Provenance-Tagged Relations panel, both agents for Nairobi and all three for Paris. To return to the notebook, if you are following one, pick 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:

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:

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:

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). 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 the configuration chapter). The query below guards the call with tool_available, so where no such compiler is installed – in particular in the Playground, 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:

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

view_circuit renders the provenance circuit as an ASCII box-art diagram using graph-easy (which must be on your PATH). The query guards the call with tool_available, so without graph-easy – in particular in the Playground, where Studio’s interactive Circuit mode is the better view anyway – it returns a message instead of failing:

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

to_provxml serialises the provenance circuit to PROV-XML, the W3C standard for provenance interchange, which can be processed by any standard XML tool:

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:

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):

-- 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;

-- 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;

-- 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;

-- 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;

-- 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, probability_evaluate returns the exact probability, and a cost-based chooser picks, for each circuit, the exact method it expects to be cheapest (see Choosing a guarantee, not a 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 $n = z^2 / (4\varepsilon^2)$ with $z = 1.96$ , $\varepsilon = 0.01$ ; see 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 $\oplus$ or $\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

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.

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 sr_formula, the provenance mapping is optional.

Step 15: Programmatic Circuit Inspection

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

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';

get_nb_gates reports how many gates the current database’s provenance circuit holds:

SELECT get_nb_gates();

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

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:

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. identify_token performs a reverse lookup, returning the table and column count for an input token:

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: set_prob refuses a different value for a token that already has one, and its error message points to replace_input, which gives the row a fresh input gate with the new probability:

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:

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:

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? 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. 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:

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. sr_minmax would answer unclassified and restricted, suggesting every higher level too. visible_at tests a single level, given as text, and 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:

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? 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:

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 sr_subset the allies to which it shows that number:

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.