rif: Phase 2 — RIF.Core.Eval fuel-bounded fixpoint with proven saturation#220
Merged
Conversation
Phase 2 of the RIF Core F* engine, layered on the Phase 1 Syntax + Translation modules already on claude/main (PR #204). One rule firing maps to a SPARQL CONSTRUCT-style operation: translate body to a BGP, evaluate via SPARQL11.Algebra.eval_bgp against the current graph, instantiate the head per binding, append new triples to the graph under set semantics. Saturated-flag pattern instead of decidable graph equality — each round returns (rdf_graph, changed:bool); fixpoint stops on changed= false or fuel exhaustion. The fuel bound is the design doc's recommended termination strategy (issue #182, docs/designissues/2026-05-07-rif-fstar-investigation.md); avoids Datalog termination theory. Saturation lemma `lemma_fixpoint_extends` proves graph_subset g (fixpoint g p fuel) — forward-chaining never removes triples. Proven by induction following the function structure: append-preserves-mem, fire_head_per_bindings, fire_rule, one_round_aux, fixpoint, plus a Classical.forall_intro / move_requires wrapper at the top. assert_norm smoke test exercises the round-trip: a 3-triple graph with subClassOf + rdf:type plus two RIF rules (subClassOf transitivity and rdf:type propagation) saturates to >= 4 triples in 8 rounds. Verified clean under z3 4.13.3 with no --lax, no --admit_smt_queries, no assume val (per CLAUDE.md rules #1, #3, #10). Issue: #182
There was a problem hiding this comment.
Pull request overview
Adds Phase 2 of the RIF Core roadmap by introducing a verified, fuel-bounded forward-chaining evaluator that reuses the existing SPARQL algebra BGP evaluation to compute rule-body bindings and materialize rule heads into an RDF graph, along with a proven “never removes triples” (monotonicity) lemma and a small assert_norm smoke test.
Changes:
- Implement
fire_rule,one_round, and a fuel-boundedfixpointsaturation loop using a(graph, changed:bool)convergence flag. - Prove
lemma_fixpoint_extends(graph subset/monotonicity) via a structured induction ladder over the evaluator’s recursion. - Add a normalization-time smoke test covering
rdfs:subClassOftransitivity andrdf:typepropagation.
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
Comment on lines
+161
to
+179
| // unchanged. Otherwise the body BGP is evaluated against the graph | ||
| // and each binding fires the head. | ||
| // ------------------------------------------------------------------ | ||
|
|
||
| let fire_rule (g : rdf_graph) (r : Syn.rif_rule) | ||
| : Tot (rdf_graph & bool) | ||
| = | ||
| match Tx.translate_body r.body with | ||
| | None -> (g, false) | ||
| | Some body_bgp -> | ||
| let bindings : solution_sequence = eval_bgp body_bgp g in | ||
| fire_head_per_bindings r.head bindings g false | ||
|
|
||
| // ------------------------------------------------------------------ | ||
| // 4. One round: fire every rule once against the current graph. | ||
| // | ||
| // Threads (graph, changed) through the rule list. The returned bool | ||
| // is OR-ed across all rules — if any rule produced a new triple, the | ||
| // round counts as changed and the fixpoint loop will iterate. |
Comment on lines
+183
to
+186
| // makes the per-round result rule-order-dependent — the fixpoint | ||
| // itself is order-independent because monotone forward-chaining | ||
| // converges to the same closure regardless of firing order. The | ||
| // design doc's "monotone, stratified" framing relies on this. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Phase 2 of the RIF roadmap (issue #182). Forward-chaining fixpoint over RDF, consuming the Phase 1 Syntax + Translation modules from #204.
formal/fstar/RIF.Core.Eval.fst— 446 LoC. Verifies clean under z3 4.13.3, no--lax, no--admit_smt_queries, noassume val.What's in scope
fire_rule : graph -> rif_rule -> graph & bool— one rule against the current graph;bool= "graph changed".one_round : graph -> rif_program -> graph & bool— one shot per rule.fixpoint : graph -> rif_program -> fuel:nat -> graph (decreases fuel)— saturated-flag fixpoint; stops onchanged=falseor fuel exhaustion.lemma_fixpoint_extends : g p fuel -> Lemma (graph_subset g (fixpoint g p fuel))— proven monotonicity. Built from a 5-step inductive ladder, no admits.assert_normsmoke test:subClassOftransitivity +rdf:typepropagation, 3 input triples → ≥4 output, reduces at elaboration.Implementation choices (worth flagging)
SPARQL11.Algebra.eval_bgp : bgp -> rdf_graph -> solution_sequenceatSPARQL11.Algebra.fst:1894. Backend-neutral; takes a plainrdf_graph. TheSPARQL11.Store.eval_bgp_backendwas the alternative but RIF's input is in-memory so the algebra one is the fit.rdf_graph = list triplehas no decidable equality inRDF.Graph.Executable.fst. Per the design-doc allowance, used the saturated-flag pattern:(graph, changed:bool)plumbed throughfire_rule/one_round/add_one_triple_tracking. Fixpoint stops onchanged=false.graph_len ... >= 4rather than exact-set membership because reducing list-basedmemthrough the eval_bgp / sm_lookup tower underassert_normtends to time-out the SMT solver while exercising the same code paths.Saturation lemma — the proof ladder
lemma_mem_triple_append_left—mem_triple t g ==> mem_triple t (g @ [u])lemma_add_one_triple_tracking_preserveslemma_fire_head_per_bindings_preserves(induction on bindings)lemma_fire_rule_preserves(case-split onTx.translate_body)lemma_one_round_aux_preserves(induction on rules)lemma_fixpoint_preserves(induction on fuel)lemma_fixpoint_extendslifts viaClassical.forall_intro+Classical.move_requires.What's NOT in this PR
Parser.RIFXML.fst(Phase 3) — concrete syntax for the W3C test inputs.RIF.Core.Tests.fst(Phase 4) — runner shim that swapsRIF-Skipatw3c_runner.ml:1935-1940.Each is its own follow-up. With Phase 1 + 2 on main, the engine is functionally complete; Phase 3 + 4 wire it to the W3C corpus to retire the 4 SPARQL skips.
Test plan
fstar.exe --z3version 4.13.3 RIF.Core.Eval.fstverifies clean.assert_normsmoke test passes.Migration
Issue #182 ticks: Phase 2 (Eval) done. Engine is functionally complete pending the parser + runner-shim sister PRs.