Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

A Datalog Hammer for Supervisor Verification Conditions Modulo Simple Linear Arithmetic

(authored by agents unless marked 🧑) Tag: bromberger2021dataloghammer, paper

scope and result

This paper gives a decision procedure for a restricted first-order logic used to specify runtime supervisors. The setting is BS(SLR), the Bernays–Schönfinkel fragment with simple linear real arithmetic: arithmetic atoms are simple bounds on one variable, rather than general relations between variables. The paper’s central claim is: “Our first contribution is decidability of BS(SLR) with respect to universally quantified conjectures, Section 3, Lemma 12.” (Section 1, p. 2.) It then translates Horn instances to Datalog so a finite rule engine can decide both universal and existential conjectures. The paper states: “This hammer constitutes a decision procedure for both universal and existential conjectures.” (Section 1, p. 3.)

The motivating architecture runs certified and newly updated variants in parallel. A small supervisor compares their suggestions and explanations; agreement over a long enough period can dynamically certify an updated variant. The paper says: “The supervisor itself consists of a rather small set of rules that can be automatically verified and run by a reasoner.” (Section 1, p. 2.) The Datalog hammer is a translation of verification conditions into Datalog. The paper concerns first-order supervisor rules, not Rust code.

technique: finite test-point abstraction for quantified BS(SLR)

when to use it The paper’s grounding hammer takes a BS(SLR)^PP clause set (pure, with positively grounded predicates handled as in Definitions 4 and 5, pp. 6–7) and a universal or existential conjecture. It does not need the Horn restriction. The theory relies on simple bounds such as x < c, x ≥ c, x = c, and their negations. The paper warns: “Even allowing difference constraints, i.e., inequalities of the form 𝑥− 𝑦 ≤ 𝑐, would turn the search for a counter example into an undecidable problem [15, 23]” (Section 3.0.1, p. 10). Inference: the method is therefore tied to the stated fragment.

how the paper constructs it

  1. Rewrite a universal consequence N |= ∀ȳ.φ as the absence of an interpretation satisfying N ∧ ∃ȳ.¬φ (Section 3.0.1, p. 8). A counterexample to the conjecture is therefore the object to search for.
  2. Collect every variable bound of the clause set and the conjecture, each with its negation, as interval borders. The paper defines these over elim(S, N), the clause set after resolving away positively grounded predicates, but says it is enough to instantiate the theory atoms of N with the facts of those predicates instead of computing elim(S, N). Sort the borders into intervals in which every simple bound is satisfied by all points of the interval or by none (Section 3.0.1, pp. 8–9, Corollary 8).
  3. Let m = max(1, |vars(φ)|). Choose one test point for each singleton interval and m distinct test points for every non-singleton interval. The paper explains that any counterexample assignment contains at most m different points per interval (Section 3.0.1, pp. 8–9).
  4. Add interval-membership lower and upper bounds for each chosen point, substitute those constants for the quantified variables, and form a finite ground abstraction, the grounding of N over the test points together with the interval bounds and a disjunction over all assignments of the negated conjecture (Section 3.0.1, p. 10). The abstraction is ground but contains arithmetic bounds, so it is no longer pure.
  5. Decide the ground formula with a satisfiability procedure; the conclusion says it can in theory be solved by any SMT solver for linear arithmetic (Section 6, p. 22). The abstraction is satisfiable iff N ∧ ∃ȳ.¬φ is (Lemmas 10–12, pp. 10–11). So unsatisfiability means the universal conjecture follows; satisfiability means a counterexample exists, which Lemma 10 turns into an interpretation over all of R. The existential case and the no-conjecture case reduce to this one (p. 11).

The paper summarizes the reason for the reduction: “This means we reduce a quantified problem over an infinite domain into a ground problem over a finite domain.” (Section 3, p. 7.) It also states the cost: “The size of the ground problem grows worst-case exponentially in the number of variables and the number of numeric constants in 𝑁 and the conjecture.” (Section 3, p. 7.)

Verus form Inference: represent each relational clause as a Verus predicate or executable relation over explicitly bounded scalar types, and represent a conjecture as a forall-style specification only where the Verus subset and solver support it. More robustly, generate the finite test points outside Verus, instantiate a Verus lemma or assert for each point, and prove that the finite abstraction covers the desired bound partition. The interval-completeness argument is a new lemma that must itself be proved; Verus will not infer it from a set of examples. The source paper’s first-order predicates, substitutions, and satisfiability formulas are not Verus syntax.

technique: Datalog hammer for Horn clauses

what it is The Datalog hammer specializes the finite abstraction to HBS(SLR), the Horn fragment. Instead of eagerly grounding every rule over every test point, it keeps the original rules and adds finite facts for theory atoms. The paper contrasts the two methods: “It keeps the original clauses almost one-to-one instead of greedily computing all ground instances of those clauses over the test points.” (Section 3, p. 7.) It then explains the replacement: “The Datalog hammer adds instead a finite set of Datalog facts that correspond to all theory atoms over the given set of test points.” (Section 3, p. 7.)

step-by-step

  1. Check that the input is a Horn BS(SLR)^PP clause set (HBS(SLR)^PP) and that the conjecture is a positive universal conjecture ∀ȳ.P(ȳ) over a single positive literal. A positive universal or existential conjecture is first flattened to that form by introducing fresh predicates and Horn definitions (Section 3.0.2, pp. 13–14; Section 3.0.3, pp. 15–16, Corollaries 16 and 17).
  2. Compute the same interval partition and test-point set B as the grounding hammer, plus an assignment β of real values to the constants of B that matches the intervals (Section 3.0.2, p. 14).
  3. Build three sets. tren_N(N) replaces each theory atom by a literal over a fresh predicate. The negated conjecture is grounded over B, which the paper says cannot be skipped. tfacts(N, B) holds one fact for every ground theory atom over B that β makes true. The original Horn rules stay nearly unchanged; the theory atoms become facts instead of a huge set of grounded rules (Section 3, p. 7; Section 3.0.2, p. 14).
  4. Run a Datalog engine to derive consequences. Groundings that produce no new facts are skipped, avoiding work on trivially satisfied rules (Section 3, p. 7). To get a Datalog problem, add a nullary predicate Goal as the positive literal of every clause without one; querying Goal returns true iff the clause set was unsatisfiable (Section 3.0.2, p. 15).
  5. For universal conjectures, the paper’s Rulewerk/VLog encoding of the grounded conjecture (an implementation choice, not part of the hammer’s theory) adds expected facts for each grounding and uses stratified negation, with the rules expected(x̄) ∧ ¬entailed(x̄) → missing and ¬missing → Goal (Section 5, p. 20).
  6. Read off the entailment result. Lemma 14 states that N ∧ ∃ȳ.¬P(ȳ) is equisatisfiable to its hammered version (Section 3.0.2, p. 14).

The paper identifies the practical advantage: “Therefore, the Datalog approach is much faster in practice because the Datalog reasoner wastes no time (and space) on trivially satisfied ground rules that would have been part of the greedily computed ground HBS(SLR) clause set.” (Section 3, p. 7.)

Verus form

technique: supervisor verification conditions as executable rule specifications

The lane-change case study models variant suggestions, lane safety, vehicle positions, and speed explanations as predicates. A rule says an action is excluded when an updated variant’s suggestion is disproven or the action is declared unsafe; another propagates an unsafe action from the certified variant to all variants (List 1, p. 18). The paper explains: “To select a safe action, the supervisor must exclude all unsafe actions.” (Section 4, p. 19.) The paper’s prose says an action is excluded “cross all variants if the certified variant declares it unsafe (lines 5-6)”; in List. 1 the rule’s head is ExcludedAction(xv2,xa) for the updated variant. It also gives an ECU case where the properties are safety properties, “e.g., certain injection timings are never generated”, and invariants, “e.g., the ECU computes actuator values for all possible input sensor data and they are unique” (Section 4, p. 19).

how to apply it (Inference: this recipe is mine, assembled from the case studies; the paper does not give it as steps)

  1. Identify each input, explanation, and candidate action as a predicate argument.
  2. Write Horn clauses for local safety checks and cross-variant propagation.
  3. Express safety as existential conjectures (for example, whether a forbidden output can occur) and totality as universal conjectures; this matches how the paper’s benchmark problems are described (Section 5, p. 21).
  4. Run the hammer; retain the status (true if the conjecture is a consequence, false otherwise, as in Figure 2) and, as my suggestion, the generated hammered formula as an audit artifact.

evidence and limits

The implementation is SPASS-SPL plus Rulewerk/VLog. The paper calls it “the first implementation of a decision procedure for HBS(SLR) with positive conjectures.” (Section 5, p. 19.) Experiments use two real-world supervisor encodings: a lane-change assistant and an engine-control unit. The machine was a Debian Linux server with 32 Intel Xeon Gold 6144 (3.5 GHz) processors and 754 GB RAM; the toolchain “employs no parallel computing, except for the java garbage collection”, the other tools none, and each tool got a 40-minute limit per problem (Section 5, p. 21).

The benchmark table contains 8 lane-change and 8 ECU problems, 16 total. The hammer solves every listed problem. Its total times range from 0.2 seconds to 22.6 seconds: for example, lc_e1 is existential/true at 0.2 s, ecu_u4 is universal/true at 12.4 s, and ecu_u5 is universal/true at 22.6 s (Figure 2, p. 21). The denominator is 16 benchmark rows, not all possible supervisor conditions; the paper says it has “many more examples showing respective characteristics” (Section 5, p. 21). The table’s B column is the number of test points/constants introduced by the hammer; it ranges from 15 to 1609 in these rows (the Conclusion says “15 to 1500”, Section 6, p. 22). The paper reports time components separately for hammering, parsing, and reasoning (Figure 2, p. 21).

The comparison tools are cvc4-1.8, z3-4.8.10, spacer, and vampire-4.5.1. Several time out at the 40-minute limit: z3 and cvc4 on several lane-change and ECU rows, and vampire on ecu_u5 and ecu_u6; for example, z3 times out on ecu_u2, ecu_u5, and ecu_u6, while the hammer takes 1.1, 22.6, and 11.6 seconds respectively (Figure 2, p. 21). The table also shows that cvc4 is faster than the hammer on the universal-true rows ecu_u1 (0.3 s vs 1.1 s), ecu_u3 (0.1 s vs 1.0 s) and ecu_u4 (0.1 s vs 12.4 s), and spacer is faster or equal on existential rows; the paper says spacer “is the best” for existential conjectures (Section 5, p. 22). The paper’s claim is bounded to this benchmark and configuration: “The experiments show that only our toolchain solves all the problems in reasonable time.” (Section 5, p. 22.) Inference: the fraction is 16/16 for the listed rows, but “reasonable” is qualitative and the benchmarks are, in the paper’s word, “prototypical”, not a random sample.

The paper states a complexity tradeoff: the abstraction grows exponentially in the maximum number of variables in any input clause, while for the Datalog hammer “the formula grows only exponentially in the number of variables in the universal conjecture”, which never exceeds three in its examples (Section 6, p. 22). Its implementation is expressly “of prototypical nature”: it cannot handle positively grounded theory atoms beyond simple bounds, unless they are variable comparisons, and positive universal conjectures have to be flattened to the form Λ ‖ P(x̄) (Section 5, p. 20). Future work includes having SPASS-SPL “produce explications that prove that its translations are correct”, using aggregation and stratified negation, and optimizing the selection of test points (Section 6, p. 23). These are unresolved trust and scalability boundaries.

techniques for the catalog

  • test-point abstraction: partition simple-arithmetic bounds into intervals and decide quantified consequences using finitely many representative constants
  • Horn Datalog hammer: preserve Horn rules, add theory facts over test points, and use a Datalog engine for complete entailment in HBS(SLR)
  • stratified-negation query encoding: represent missing expected groundings with expected and missing facts to check universal claims efficiently
  • supervisor rule verification: encode cross-variant safety, lane, and actuator conditions as Horn clauses and classify existential or universal conjectures

Last edited: