{ "nbformat": 4, "nbformat_minor": 5, "metadata": { "kernelspec": { "name": "provsql-studio", "display_name": "ProvSQL (SQL)", "language": "sql" }, "language_info": { "name": "sql" }, "provsql": { "scheme": "semiring", "database": "cs1", "generated_from": "doc/source/user/casestudy1.rst" } }, "cells": [ { "cell_type": "markdown", "metadata": {}, "source": [ "# Case Study: Intelligence Agency\n", "\n", "This case study largely extends the scenario of the paper that first presented ProvSQL. Through a security-classification scenario, it demonstrates custom semirings, clearance levels under negation, where-provenance, probability computation with several algorithms, and circuit export.\n", "\n", "## The Scenario\n", "\n", "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:\n", "\n", "- identify which cities are served by more than one agent,\n", "- determine the minimum clearance level needed to infer each result,\n", "- find cities with exactly one agent (sensitive: whatever is traced back to that city’s station points to the one agent there),\n", "- track where in the database each output value originated,\n", "- compute the probability that a city remains a single-agent post after accounting for possible-world uncertainty,\n", "- find at which clearance levels an analyst would wrongly conclude that a city has a single agent, and which allied services would.\n", "\n", "## Setup" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "*The following cells set up the database with all the content this notebook requires; run them first, ideally on a fresh database.*" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "DROP TYPE IF EXISTS classification_level CASCADE;\n", "CREATE TYPE classification_level AS ENUM (\n", " 'unclassified', 'restricted', 'confidential', 'secret', 'top_secret',\n", " 'unavailable'\n", ");" ], "outputs": [] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "DROP TABLE IF EXISTS personnel CASCADE;\n", "CREATE TABLE personnel (\n", " id SERIAL PRIMARY KEY,\n", " name TEXT NOT NULL,\n", " position TEXT NOT NULL,\n", " city TEXT NOT NULL,\n", " classification classification_level NOT NULL\n", ");" ], "outputs": [] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "TRUNCATE personnel;\n", "INSERT INTO personnel (name, position, city, classification) VALUES\n", " ('Juma', 'Director', 'Nairobi', 'unclassified'),\n", " ('Paul', 'Janitor', 'Nairobi', 'restricted'),\n", " ('David', 'Analyst', 'Paris', 'confidential'),\n", " ('Ellen', 'Field agent', 'Beijing', 'secret'),\n", " ('Aaheli', 'Double agent', 'Paris', 'top_secret'),\n", " ('Nancy', 'HR', 'Paris', 'restricted'),\n", " ('Jing', 'Analyst', 'Beijing', 'secret');" ], "outputs": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "This creates:\n", "\n", "- `classification_level` – an ordered ENUM (`unclassified` \\< `restricted` \\< `confidential` \\< `secret` \\< `top_secret` \\< `unavailable`) where `unavailable` is a sentinel representing the semiring 𝟘 (no derivation possible)\n", "- `personnel` – 7 agents with name, position, city, and the classification level of their record\n", "\n", "## Step 1: Explore the Database\n", "\n", "Inspect the `personnel` table:" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "SELECT * FROM personnel ORDER BY id;" ], "outputs": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "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).\n", "\n", "## Step 2: Enable Provenance and Create a Name Mapping\n", "\n", "Enable provenance tracking on `personnel` and create a mapping so that provenance tokens can be labelled with agent names:" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "SELECT add_provenance('personnel');\n", "DROP TABLE IF EXISTS personnel_name;\n", "SELECT create_provenance_mapping('personnel_name', 'personnel', 'name');" ], "outputs": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "After [`add_provenance`](https://provsql.org/doxygen-sql/html/group__table__management.html#ga00f0d0b04b2b693c974e72aaf095cb3b), 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.\n", "\n", "## Step 3: Cities Shared by Multiple Agents\n", "\n", "Which cities have at least two agents? Use a self-join with an `id` inequality to generate all unordered pairs, then apply [`sr_formula`](https://provsql.org/doxygen-sql/html/group__compiled__semirings.html#gae49f63c94b0094be6756f2f42d4caecd) to see which agents contribute to each city:" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "SELECT p1.city,\n", " sr_formula(provenance(), 'personnel_name') AS formula\n", "FROM personnel p1\n", "JOIN personnel p2 ON p1.city = p2.city AND p1.id < p2.id\n", "GROUP BY p1.city\n", "ORDER BY p1.city;" ], "outputs": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "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 `⊕`.\n", "\n", "## Step 4: Minimum Security Clearance (sr_minmax)\n", "\n", "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.\n", "\n", "The min-max m-semiring, available as [`sr_minmax`](https://provsql.org/doxygen-sql/html/group__compiled__semirings.html#ga1861588ff5f551d207f332bccab4626c), answers this over the `classification_level` enum:\n", "\n", "- `⊕` (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).\n", "- `⊗` (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).\n", "\n", "The third argument gives the carrier enum: only its type is used, so it is written `NULL::classification_level`:" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "DROP TABLE IF EXISTS personnel_level;\n", "SELECT create_provenance_mapping('personnel_level',\n", " 'personnel', 'classification');\n", "\n", "SELECT p1.city,\n", " sr_minmax(provenance(), 'personnel_level',\n", " NULL::classification_level) AS min_clearance\n", "FROM personnel p1\n", "JOIN personnel p2 ON p1.city = p2.city AND p1.id < p2.id\n", "GROUP BY p1.city\n", "ORDER BY p1.city;" ], "outputs": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "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.\n", "\n", "## Step 5: Cities with Exactly One Agent (EXCEPT / Monus)\n", "\n", "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`:" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "SELECT city,\n", " sr_formula(provenance(), 'personnel_name') AS formula\n", "FROM (\n", " SELECT DISTINCT city FROM personnel\n", " EXCEPT\n", " SELECT p1.city\n", " FROM personnel p1\n", " JOIN personnel p2 ON p1.city = p2.city AND p1.id < p2.id\n", " GROUP BY p1.city\n", ") t\n", "ORDER BY city;" ], "outputs": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "**Note:**\n", "\n", "> 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.”\n", "\n", "## Step 6: Where-Provenance\n", "\n", "Where-provenance tracks *which column of which input row* produced each output value. Enable it and re-run the shared-city query:" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "SET provsql.provenance = 'where';\n", "\n", "SELECT p1.city,\n", " where_provenance(provenance()) AS source\n", "FROM personnel p1\n", "JOIN personnel p2 ON p1.city = p2.city AND p1.id < p2.id\n", "GROUP BY p1.city\n", "ORDER BY p1.city;\n", "\n", "SET provsql.provenance = 'semiring';" ], "outputs": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "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.\n", "\n", "### Seeing it in Studio: Where mode\n", "\n", "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.\n", "\n", "## Step 7: Assign Probabilities\n", "\n", "Suppose the existence of each agent in the database is uncertain. Assign each agent a probability equal to `id / 10.0`:" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "SELECT set_prob(provenance(), id / 10.0) FROM personnel;" ], "outputs": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Now Juma has probability 0.1, Paul 0.2, and so on up to Jing 0.7.\n", "\n", "## Step 8: Probability – Exact\n", "\n", "Compute the exact probability that each city is a single-agent city:" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "SELECT city,\n", " ROUND(probability_evaluate(provenance())::numeric, 4) AS prob\n", "FROM (\n", " SELECT DISTINCT city FROM personnel\n", " EXCEPT\n", " SELECT p1.city\n", " FROM personnel p1\n", " JOIN personnel p2 ON p1.city = p2.city AND p1.id < p2.id\n", " GROUP BY p1.city\n", ") t\n", "ORDER BY city;" ], "outputs": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "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`.\n", "\n", "## Step 9: Probability – Monte Carlo\n", "\n", "For larger circuits, exact evaluation can be expensive. Monte Carlo sampling gives an approximate answer:" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "SELECT city,\n", " probability_evaluate(\n", " provenance(), 'monte-carlo', '10000') AS prob\n", "FROM (\n", " SELECT DISTINCT city FROM personnel\n", " EXCEPT\n", " SELECT p1.city\n", " FROM personnel p1\n", " JOIN personnel p2 ON p1.city = p2.city AND p1.id < p2.id\n", " GROUP BY p1.city\n", ") t\n", "ORDER BY city;" ], "outputs": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "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).\n", "\n", "## Step 10: Probability – Knowledge Compiler\n", "\n", "**Note:**\n", "\n", "> 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](https://provsql.org/docs/user/configuration.html)). The query below guards the call with [`tool_available`](https://provsql.org/doxygen-sql/html/group__provenance__output.html#ga4ae4f9f7a08be9333e78028fe10bd6cc), 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.\n", "\n", "A knowledge compiler converts the provenance circuit to a *d-DNNF* representation, which enables efficient exact probability evaluation on large circuits of specific forms:" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "SELECT city,\n", " CASE WHEN tool_available('d4')\n", " THEN ROUND(probability_evaluate(\n", " provenance(), 'compilation', 'd4')::numeric, 4)::text\n", " ELSE '(needs external compiler d4; unavailable here)'\n", " END AS prob\n", "FROM (\n", " SELECT DISTINCT city FROM personnel\n", " EXCEPT\n", " SELECT p1.city\n", " FROM personnel p1\n", " JOIN personnel p2 ON p1.city = p2.city AND p1.id < p2.id\n", " GROUP BY p1.city\n", ") t\n", "ORDER BY city;" ], "outputs": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "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.\n", "\n", "## Step 11: Visualise a Provenance Circuit\n", "\n", "[`view_circuit`](https://provsql.org/doxygen-sql/html/group__provenance__output.html#ga1c6caf1bb91c0cfdfc56c33666d41897) 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 [`tool_available`](https://provsql.org/doxygen-sql/html/group__provenance__output.html#ga4ae4f9f7a08be9333e78028fe10bd6cc), so without `graph-easy` – in particular in the Playground, where Studio’s interactive [Circuit mode](https://provsql.org/docs/user/studio.html) is the better view anyway – it returns a message instead of failing:" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "SELECT city,\n", " CASE WHEN tool_available('graph-easy')\n", " THEN view_circuit(provenance(), 'personnel_name')\n", " ELSE '(needs the graph-easy renderer; use Studio Circuit mode)'\n", " END AS circuit\n", "FROM (\n", " SELECT DISTINCT city FROM personnel\n", " EXCEPT\n", " SELECT p1.city\n", " FROM personnel p1\n", " JOIN personnel p2 ON p1.city = p2.city AND p1.id < p2.id\n", " GROUP BY p1.city\n", ") t\n", "WHERE city = 'Nairobi';" ], "outputs": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "The result shows the monus gate at the top, with `Juma` and `Paul` as leaf inputs, rendered in box-art notation in the terminal.\n", "\n", "## Step 12: Export to XML\n", "\n", "[`to_provxml`](https://provsql.org/doxygen-sql/html/group__provenance__output.html#gacc9e8b2a47ade6f5c87c27f64b4707b1) 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:" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "SELECT city,\n", " to_provxml(provenance(), 'personnel_name') AS provxml\n", "FROM (\n", " SELECT DISTINCT city FROM personnel\n", " EXCEPT\n", " SELECT p1.city\n", " FROM personnel p1\n", " JOIN personnel p2 ON p1.city = p2.city AND p1.id < p2.id\n", " GROUP BY p1.city\n", ") t\n", "WHERE city = 'Nairobi';" ], "outputs": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Step 13: Large Circuit Benchmark\n", "\n", "To compare the three probability algorithms at scale, create a synthetic 100 × 100 random-probability matrix and enable provenance tracking on it:" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "DROP TABLE IF EXISTS matrix CASCADE;\n", "CREATE TABLE matrix AS\n", "SELECT ones.n + 10 * tens.n AS x,\n", " other.n + 10 * tens2.n AS y,\n", " random() AS prob\n", "FROM (VALUES(0),(1),(2),(3),(4),(5),(6),(7),(8),(9)) ones(n),\n", " (VALUES(0),(1),(2),(3),(4),(5),(6),(7),(8),(9)) tens(n),\n", " (VALUES(0),(1),(2),(3),(4),(5),(6),(7),(8),(9)) other(n),\n", " (VALUES(0),(1),(2),(3),(4),(5),(6),(7),(8),(9)) tens2(n);\n", "\n", "SELECT add_provenance('matrix');\n", "SELECT set_prob(provenance(), prob) FROM matrix;" ], "outputs": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "The last query returns one (empty) row per cell of the matrix, 10,000 in all.\n", "\n", "Now run the same path query with each method in turn, timing each (`\\timing` in psql, or Studio’s per-query timing):" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "-- No method named: the exact probability, by the method expected to\n", "-- be cheapest on each row's circuit\n", "SET provsql.last_eval_method = '';\n", "SELECT m1.x, m2.y,\n", " probability_evaluate(provenance()) AS prob\n", "FROM matrix m1, matrix m2\n", "WHERE m2.x = m1.y AND m1.x > 90 AND m2.x > 90 AND m2.y > 90\n", "GROUP BY m1.x, m2.y\n", "ORDER BY m1.x, m2.y;\n", "\n", "SHOW provsql.last_eval_method;" ], "outputs": [] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "-- Exact enumeration over all possible worlds\n", "SELECT m1.x, m2.y,\n", " probability_evaluate(provenance(), 'possible-worlds') AS prob\n", "FROM matrix m1, matrix m2\n", "WHERE m2.x = m1.y AND m1.x > 90 AND m2.x > 90 AND m2.y > 90\n", "GROUP BY m1.x, m2.y\n", "ORDER BY m1.x, m2.y;" ], "outputs": [] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "-- Monte Carlo sampling (9604 samples ≈ 1 % error at 95 % confidence)\n", "SELECT m1.x, m2.y,\n", " probability_evaluate(provenance(), 'monte-carlo', '9604') AS prob\n", "FROM matrix m1, matrix m2\n", "WHERE m2.x = m1.y AND m1.x > 90 AND m2.x > 90 AND m2.y > 90\n", "GROUP BY m1.x, m2.y\n", "ORDER BY m1.x, m2.y;" ], "outputs": [] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "-- Tree-decomposition-based exact compilation (built-in, no external tool)\n", "SELECT m1.x, m2.y,\n", " probability_evaluate(provenance(), 'tree-decomposition') AS prob\n", "FROM matrix m1, matrix m2\n", "WHERE m2.x = m1.y AND m1.x > 90 AND m2.x > 90 AND m2.y > 90\n", "GROUP BY m1.x, m2.y\n", "ORDER BY m1.x, m2.y;" ], "outputs": [] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "-- Knowledge compilation via external tool d4 (guarded with\n", "-- tool_available, so it reports rather than fails where d4 is\n", "-- absent, e.g. in the Playground)\n", "SELECT m1.x, m2.y,\n", " CASE WHEN tool_available('d4')\n", " THEN probability_evaluate(provenance(), 'compilation', 'd4')::text\n", " ELSE '(d4 unavailable here)'\n", " END AS prob\n", "FROM matrix m1, matrix m2\n", "WHERE m2.x = m1.y AND m1.x > 90 AND m2.x > 90 AND m2.y > 90\n", "GROUP BY m1.x, m2.y\n", "ORDER BY m1.x, m2.y;" ], "outputs": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "With no method named, [`probability_evaluate`](https://provsql.org/doxygen-sql/html/group__probability.html#gabffa40fef0e37a75d39d4c39c4a1ec0f) returns the exact probability, and a cost-based chooser picks, for each circuit, the exact method it expects to be cheapest (see `probability-guarantees`). 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.\n", "\n", "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](https://en.wikipedia.org/wiki/Margin_of_error)).\n", "\n", "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.\n", "\n", "`'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.\n", "\n", "## Step 14: The Boolean Expression Behind a Token\n", "\n", "[`sr_boolexpr`](https://provsql.org/doxygen-sql/html/group__compiled__semirings.html#ga41016a3000b008b59848687485b79425) 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." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "SELECT city, sr_boolexpr(provenance()) AS boolexpr\n", "FROM (\n", " SELECT DISTINCT city FROM personnel\n", " EXCEPT\n", " SELECT p1.city\n", " FROM personnel p1\n", " JOIN personnel p2 ON p1.city = p2.city AND p1.id < p2.id\n", " GROUP BY p1.city\n", ") t\n", "WHERE city = 'Nairobi';" ], "outputs": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "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`](https://provsql.org/doxygen-sql/html/group__compiled__semirings.html#gae49f63c94b0094be6756f2f42d4caecd), the provenance mapping is optional.\n", "\n", "## Step 15: Programmatic Circuit Inspection\n", "\n", "What [`view_circuit`](https://provsql.org/doxygen-sql/html/group__provenance__output.html#ga1c6caf1bb91c0cfdfc56c33666d41897) renders, you can also walk programmatically with the low-level circuit API. Capture Nairobi’s monus token first:" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "CREATE TEMP TABLE nairobi_token AS\n", "SELECT provenance() AS prov\n", "FROM (\n", " SELECT DISTINCT city FROM personnel\n", " EXCEPT\n", " SELECT p1.city\n", " FROM personnel p1\n", " JOIN personnel p2 ON p1.city = p2.city AND p1.id < p2.id\n", " GROUP BY p1.city\n", ") t\n", "WHERE city = 'Nairobi';" ], "outputs": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "[`get_nb_gates`](https://provsql.org/doxygen-sql/html/group__gate__manipulation.html#gad694ac39c8517985d39ac6c5fff72d80) reports how many gates the current database’s provenance circuit holds:" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "SELECT get_nb_gates();" ], "outputs": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "[`get_gate_type`](https://provsql.org/doxygen-sql/html/group__gate__manipulation.html#ga26773255355efc79f91d3109316bdb8b) and [`get_children`](https://provsql.org/doxygen-sql/html/group__gate__manipulation.html#gad2e6746782ac5b6500ebb8c48f75303b) give a single-step view of the gate structure: they return the operator and direct children of a gate." ] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "SELECT get_gate_type(prov) AS root_type,\n", " get_children(prov) AS root_children\n", "FROM nairobi_token;" ], "outputs": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "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:" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "SELECT (get_children(prov))[1] AS plus_token,\n", " get_gate_type((get_children(prov))[1]) AS plus_type,\n", " get_children((get_children(prov))[1]) AS plus_children\n", "FROM nairobi_token;" ], "outputs": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "The leaves of the circuit are input gates that originate from the `personnel` table. [`identify_token`](https://provsql.org/doxygen-sql/html/group__circuit__introspection.html#gad53f5ec3f9c5d86714dd6299e5a5185e) performs a reverse lookup, returning the table and column count for an input token:" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "SELECT identify_token(child) AS source\n", "FROM nairobi_token, unnest(get_children((get_children(prov))[1])) AS child;" ], "outputs": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Both leaves resolve to `(personnel, 5)`: the `personnel` table with its five non-provenance columns (`id`, `name`, `position`, `city` and `classification`).\n", "\n", "## Step 16: Revising a Probability\n", "\n", "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`](https://provsql.org/doxygen-sql/html/group__gate__manipulation.html#ga17334fe1d3969d969eaa18e32a93b4e0) refuses a different value for a token that already has one, and its error message points to [`replace_input`](https://provsql.org/doxygen-sql/html/group__gate__manipulation.html#ga416b70eb6e5156b435a90a695f3cc564), which gives the row a fresh input gate with the new probability:" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "UPDATE personnel SET provsql = replace_input(provsql, 0.9)\n", "WHERE name = 'Juma';" ], "outputs": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "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:" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "SELECT city,\n", " ROUND(probability_evaluate(provenance())::numeric, 4) AS prob\n", "FROM (\n", " SELECT DISTINCT city FROM personnel\n", " EXCEPT\n", " SELECT p1.city\n", " FROM personnel p1\n", " JOIN personnel p2 ON p1.city = p2.city AND p1.id < p2.id\n", " GROUP BY p1.city\n", ") t\n", "ORDER BY city;" ], "outputs": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "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`:" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "SELECT ROUND(probability_evaluate(prov)::numeric, 4) AS prob\n", "FROM nairobi_token;" ], "outputs": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Step 17: Clearance Levels of a Negation\n", "\n", "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`](https://provsql.org/doxygen-sql/html/group__compiled__semirings.html#ga1861588ff5f551d207f332bccab4626c) (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`](https://provsql.org/doxygen-sql/html/group__compiled__semirings.html#gab690e03dd71d1a95c12514319cdf7b6b) 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:" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "DROP TABLE IF EXISTS personnel_level;\n", "SELECT create_provenance_mapping('personnel_level',\n", " 'personnel', 'classification');\n", "\n", "SELECT city,\n", " sr_clearance(provenance(), 'personnel_level',\n", " NULL::classification_level) AS levels,\n", " visible_at(provenance(), 'personnel_level', 'unclassified')\n", " AS at_unclassified,\n", " (clearance_settling(provenance(), 'personnel_level',\n", " NULL::classification_level)).*\n", "FROM (\n", " SELECT DISTINCT city FROM personnel\n", " EXCEPT\n", " SELECT p1.city\n", " FROM personnel p1\n", " JOIN personnel p2 ON p1.city = p2.city AND p1.id < p2.id\n", " GROUP BY p1.city\n", ") t\n", "ORDER BY city;" ], "outputs": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "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`](https://provsql.org/doxygen-sql/html/group__compiled__semirings.html#ga1861588ff5f551d207f332bccab4626c) would answer `unclassified` and `restricted`, suggesting every higher level too. [`visible_at`](https://provsql.org/doxygen-sql/html/group__compiled__semirings.html#gad69d1770f84af45ec9476b430fb24e4d) tests a single level, given as text, and [`clearance_settling`](https://provsql.org/doxygen-sql/html/group__compiled__semirings.html#ga53ecac1843b6bc3ccecac3ff0e5cbe28) gives the level from which the answer no longer changes (`restricted` for Nairobi, `confidential` for Paris) and that answer at the top level.\n", "\n", "## Step 18: What Allied Services Conclude\n", "\n", "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:" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "DROP TABLE IF EXISTS personnel_shared;\n", "ALTER TABLE personnel DROP COLUMN IF EXISTS shared_with;\n", "DROP TYPE IF EXISTS ally;\n", "CREATE TYPE ally AS ENUM ('bnd', 'dgse', 'mi6');\n", "ALTER TABLE personnel ADD COLUMN shared_with ally[];\n", "UPDATE personnel\n", "SET shared_with = CASE name WHEN 'Juma' THEN '{mi6,dgse}'\n", " WHEN 'Paul' THEN '{mi6}'\n", " WHEN 'David' THEN '{dgse,bnd}'\n", " WHEN 'Ellen' THEN '{bnd}'\n", " WHEN 'Aaheli' THEN '{}'\n", " WHEN 'Nancy' THEN '{mi6,dgse,bnd}'\n", " WHEN 'Jing' THEN '{dgse}' END::ally[];\n", "\n", "SELECT name, city, shared_with FROM personnel ORDER BY id;" ], "outputs": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "How many agents does each ally see in each city? [`sr_subset`](https://provsql.org/doxygen-sql/html/group__compiled__semirings.html#gab973cd80960d35df49da27bf69a1137b) 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:" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "SELECT create_provenance_mapping('personnel_shared',\n", " 'personnel', 'shared_with');" ], "outputs": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Grouping the cities by their number of agents gives one row per number a city can show, and [`sr_subset`](https://provsql.org/doxygen-sql/html/group__compiled__semirings.html#gab973cd80960d35df49da27bf69a1137b) the allies to which it shows that number:" ] }, { "cell_type": "code", "execution_count": null, "metadata": { "provsql": {} }, "source": [ "SELECT city, n AS agents,\n", " sr_subset(provenance(), 'personnel_shared', NULL::ally) AS allies\n", "FROM (SELECT city, count(*) AS n FROM personnel GROUP BY city) t\n", "GROUP BY city, n\n", "ORDER BY city, agents DESC;" ], "outputs": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "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." ] } ] }