A rule reads what a rule concluded

[WaylandYang]

Cut 1 of #477. Stacked on #484.

docs/decisions/0027-a-rule-may-read-what-a-rule-concluded.md, plus its index row. No code — this is the argument, so it can be disagreed with before the runner is written.

A gas-bearing well with a completion date is a producer. That second criterion cannot be written today: a rule's conclusion is not something another rule can read, so the hydrocarbon condition gets copied into the producer rule and two rules end up sharing a premise that nothing in the base says they share.

The objection this has to answer is written into the fact_derivations DDL by 0013: premises are always assertions, or a re-run depends on what the last round left behind. The record does not waive it. The feedback happens inside one materialize() call, in memory — a fixed point that starts from the asserted facts every time and never queries derived_facts as input. A run stays a pure function of (facts, rules, axioms), which is what that objection was actually protecting; it does not follow from "premises are assertions", it follows from "the run does not read its own past output", and those coincided only while there was one pass.

What the record settles:

• A fixed point, not an ordering — MAX_DEPTH rounds, sorted frontier, same shape as derive(), because otherwise whether A → B → C fires depends on rule load order.
• A derived typing enters as a premise, not as a filter. entities.type_id carries no interval, but a derived membership does — an entity that is a B from 2019 to 2022 must not satisfy a B rule on a 2024 reading. Putting the typing in the premise list makes validity() narrow the conclusion for free, and is what makes retirement work with no code written for it.
• A rule may read its own conclusions. Forbidding it needs a rule-dependency graph that cannot be computed (a rule's inputs are predicates, not rules). The loop is safe: the derivable space is finite, rounds only add, and a repeated key never re-enters the frontier.
• The proof becomes a tree. fact_derivations gains a nullable premise_derived_id with a CHECK that exactly one premise column is set, and proof() becomes a walk. The ProofStep comment that says otherwise changes with it.
• Retirement cascades and costs nothing — recompute is total, so a chain whose leaf changed simply is not rebuilt and falls out of wanted in the same statement.
• Row identity resolves after the diff: the fixed point carries provisional ids, and premise ids are rewritten to final row ids before derivations are written.

Two open points are named rather than hidden: a kept row can keep a stale proof (already true with asserted premises, easier to hit with chains), and how deep a proof is worth drawing.

Runner and real-database tests for A → B → C, for a cycle, and for a leaf reading taking the chain with it are the next cut.

🤖 Generated with Claude Code

[WaylandYang]

Cut 2 landed on the same branch: the runner.

• The fixed point lives in materialize(). Each round evaluates every rule against a pool that starts as the asserted attribute facts and grows with the round's conclusions; it stops when a round produces no new key. Bounded by MAX_DEPTH, and rules now load ORDER BY r.id so which proof wins a tie does not depend on hash order.
• A concluded typing joins the subject scope as a condition, not a filter. scoped_by_conclusion() appends an is_a in {…} condition to every group — scope AND ((A and B) or C) distributes to (scope and A and B) or (scope and C), so 0026's one level of disjunction is preserved. The derived typing therefore lands in the premise list and validity() narrows the conclusion to the window the entity actually was a B. An asserted entities.type_id has no interval and stays a filter.
• Migration 0040 makes premise_fact_id nullable, adds premise_derived_id, and CHECKs exactly one. It also adds a derivation_premises view, because six places read premises and writing JOIN facts … UNION ALL JOIN derived_facts … six times means one of them silently lists a premise short.
• proof() walks the tree. ProofStep gains derived and a nested premises.
• Row identity resolves after the diff, as the record describes, and derivations are written in a second pass — a chained premise can point at another row in the same batch, and wanted is a HashMap with no order to rely on.
• The kept-row stale proof is closed, not deferred: the run reads the stored premises of every kept row in one query and rewrites the ones that differ (reproved in the report).

Five database tests in crates/utopia-store/tests/a_rule_reads_what_a_rule_concluded.rs:

• Well → GasBearingWell → Producer chains, and the producer's premises are one asserted (premise_fact_id) and one derived (premise_derived_id), with proof() expanding the derived step one level further.
• A concluded class holds only where it was concluded: gas-bearing 2020–2021 plus a 2022 completion reading gives no producer.
• Raising the first rule's threshold retires both rows in one pass, with nothing written to make the cascade happen.
• A rule reading its own conclusion settles well short of MAX_DEPTH — the second round reproduces a key it already has.
• A conclusion whose reading was replaced keeps its row and gets a new proof.

cargo fmt --check, cargo clippy --workspace --all-targets -- -D warnings and the full suite (68 test binaries) are clean against a real database.

The record's status line and its README row are updated; the "kept row can keep a stale proof" open point is struck through as closed.

Still cut 3: the rule table saying which rules feed which, and the entity panel drawing a proof more than one level deep.