Modes for controlling irrelevant axiom removal

Strata/Languages/Boogie/Axiom.lean

@@ -28,6 +28,7 @@ the responsibility of the user to ensure that they are consistent.
 structure Axiom where
   name : BoogieLabel
   e : LExpr BoogieLParams.mono
+  deriving Inhabited
 
 instance : ToFormat (BoogieLParams.mono : LExprParamsT).base.Identifier :=
   show ToFormat BoogieIdent from inferInstance

Strata/Languages/Boogie/CallGraph.lean

@@ -52,6 +52,10 @@ partial def CallGraph.getCallersClosure (cg : CallGraph) (name : String) : List
         go (head :: visited) (newCallers ++ tail)
   (go [] [name]).filter (· ≠ name)
 
+/-- Compute transitive closure of callers for multiple `names`. -/
+def CallGraph.getAllCallersClosure (cg : CallGraph) (names : List String) : List String :=
+  names.flatMap (cg.getCallersClosure ·)
+
 /-- Build call graph from name-calls pairs -/
 def buildCallGraph (items : List (String × List String)) : CallGraph :=
   let calleeMap := items.foldl (fun acc (name, calls) =>
@@ -131,38 +135,15 @@ def Program.toFunctionCG (prog : Program) : FunctionCG :=
 
 ---------------------------------------------------------------------
 
+abbrev FuncAxMap := Std.HashMap String (List String)
+
 /--
-Function to _relevant_ axioms mapping
-
-For now, our definition of a "relevant axiom" is quite weak: an axiom `a` is
-relevant for a function `f` if `f` occurs in the body of `a`, including in any
-trigger expressions.
-
-Eventually, we will compute a transitive closure involving both axioms and
-functions. E.g., consider the following example that we don't handle yet:
-
-```
-axiom1 : forall x :: g(x) == false
-axiom2 : forall x :: f(x) == g(x)
-----------------------------------
-goal : forall x, f(x) == true
-```
-
-Right now, we will determine that only `axiom2` is relevant for the goal, which
-means that the solver will return `unknown` in this case instead of `failed`.
-
-Note: one way to make the dependency analysis better right now is to use the
-triggers to mention relevant functions. E.g., now `axiom1` has `f` in its body,
-so it is relevant for the goal.
-
-```
-axiom1 : forall x :: {f(x)} g(x) == false
-axiom2 : forall x :: f(x) == g(x)
-----------------------------------
-goal : forall x, f(x) == true
-```
+Map from functions to their _immediately_ relevant axioms. An axiom `a` is
+_immediately_ relevant for a function `f` if `f` occurs in the body of `a`,
+including in any trigger expressions. Callees and callers of `f` are not
+associated with `a` in this map.
 -/
-def Program.toFunctionAxiomMap (prog : Program) : Std.HashMap String (List String) :=
+def Program.functionImmediateAxiomMap (prog : Program) : FuncAxMap :=
   let axioms := prog.decls.filterMap (fun decl =>
     match decl with
     | .ax a _ => some a
@@ -178,24 +159,53 @@ def Program.toFunctionAxiomMap (prog : Program) : Std.HashMap String (List Strin
       acc.insert funcName (ax.name :: existing).dedup)
     Std.HashMap.emptyWithCapacity
 
-instance : Std.ToFormat (Std.HashMap String (List Axiom)) where
-  format m :=
-    let entries :=
-      m.toList.map
-        (fun (k, v) => f!"{k}: [{Std.Format.joinSep (v.map Std.format) ", "}]")
-    f!"{Std.Format.joinSep entries ", \n"}"
+/-- Fixed-point computation for axiom relevance. -/
+private partial def computeRelevantAxioms (prog : Program) (cg : CallGraph) (fmap : FuncAxMap)
+    (relevantFunctions discoveredAxioms : List String) : List String :=
+  -- Get axioms for current relevant functions.
+  let newAxioms := relevantFunctions.flatMap (fun fn => fmap.getD fn []) |>.dedup
+  let newAxioms := newAxioms.filter (fun a => a ∉ discoveredAxioms)
+
+  if newAxioms.isEmpty then discoveredAxioms
+  else
+    let allAxioms := (discoveredAxioms ++ newAxioms).dedup
+
+    -- Find functions mentioned in newly discovered axioms.
+    let newFunctions := newAxioms.flatMap (fun axName =>
+      match prog.getAxiom? ⟨axName, .unres⟩ with
+      | some ax => (Lambda.LExpr.getOps ax.e).map (fun x => BoogieIdent.toPretty x)
+      | none => [])
+
+    -- Expand with call graph neighbors.
+    let expandedFunctions := newFunctions.flatMap (fun fn =>
+      fn :: cg.getCalleesClosure fn ++ cg.getCallersClosure fn) |>.dedup
+
+    let updatedRelevantFunctions := (relevantFunctions ++ expandedFunctions).dedup
+    computeRelevantAxioms prog cg fmap updatedRelevantFunctions allAxioms
+
+/-- Compute all axioms relevant to function `f`. An axiom `a` is relevant to a
+  function `f` if:
+
+1. `f` is present in the body of `a`.
+2. A callee of `f` is present in the body of `a`.
+3. A caller of `f` is present in the body of `a`.
+4. If there exists an axiom `b` such that `b` contains a function `g` relevant
+   to `a`.
+ -/
+def Program.getRelevantAxioms (prog : Program) (f : String) : List String :=
+  let cg := Program.toFunctionCG prog
+  let fmap := Program.functionImmediateAxiomMap prog
+  -- Start with `f` and its call graph neighbors.
+  let initialFunctions := (f :: cg.getCalleesClosure f ++ cg.getCallersClosure f).dedup
+  computeRelevantAxioms prog cg fmap initialFunctions []
 
 def Program.getIrrelevantAxioms (prog : Program) (functions : List String) : List String :=
-  let functionsSet := functions.toArray.qsort (· < ·) -- Sort for binary search
-  prog.decls.filterMap (fun decl =>
+  let allAxioms := prog.decls.filterMap (fun decl =>
     match decl with
-    | .ax a _ =>
-      let ops := Lambda.LExpr.getOps a.e
-      let hasRelevantOp := ops.any (fun op =>
-        functionsSet.binSearch (BoogieIdent.toPretty op) (· < ·) |>.isSome)
-      if hasRelevantOp then none else some a.name
+    | .ax a _ => some a.name
     | _ => none)
+  let relevantAxioms := functions.flatMap (fun f => prog.getRelevantAxioms f) |>.dedup
+  allAxioms.filter (fun a => a ∉ relevantAxioms)
 
 ---------------------------------------------------------------------
-
 end Boogie

Strata/Languages/Boogie/Options.lean

@@ -4,13 +4,74 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
+/--
+Remove irrelevant axioms; this mode is intended only for _deductive verification_,
+where it is always sound to remove an axiom. We can use this mode to prune the
+goals as a part of a backend portfolio one day to optimize verification
+performance.
+
+Soundness has the usual definition: if we report that a formula is valid, then
+it is really valid.
+
+For this discussion, we assume that there is no contradiction in the axioms.
+
+## Deductive Verification
+
+Consider a goal `G: P ==> Q`, where `P` contains an axiom/assumption `A`. If `A`
+is removed, then we get `G': P' ==> Q`, where `P'` is a weaker version of `P`
+that doesn't contain `A` (and of course, `G'` is a stronger version of `G`). For
+soundness w.r.t. deductive verification, we want: if `G'` is valid, then `G`
+was valid (but not necessarily the converse).
+
+**Case 1: `G'` is valid.**
+Since `P' ==> P`, we have `P ==> Q`, i.e., `G` is valid too. Soundness is
+preserved.
+
+**Case 2: `G'` is invalid.**
+There exists a model `M` for which `G'` is false, i.e., `M ⊨ P'` but `M ⊭ Q`.
+This alone doesn't tell us about the validity of `G`:
+- If `M ⊨ P` (i.e., `M` also satisfies the removed axiom `A`), then `M` is a
+  counterexample for `G` too, so `G` is invalid too. Thus, a counterexample can
+  be validated by checking if it satisfies `P`.
+- If `M ⊭ P` (i.e., `M` violates the removed axiom `A`), then `M` is not a
+  valid counterexample for `G`, and `G` might still be valid.
+
+**Case 3: Validity of `G'` cannot be determined.**
+This can be due to various reasons, like solver timeout, problem's complexity,
+or incomplete solver theories. `G` could be valid, invalid, or undecidable.
+
+**Soundness guarantee:** Axiom removal does not lead to proofs of
+invalid goals, but it may cause valid goals to become unprovable,
+resulting in "unknown" results. Moreover, if a counterexample is found for the
+weakened goal, it may not be a valid counterexample for the original goal.
+
+Note though that soundness is preserved regardless of the quality of axiom
+relevance analysis.
+-/
+inductive IrrelevantAxiomsMode where
+  /--
+    Only the functions in the consequent `Q` of a goal `P ==> Q` will be
+    taken into account for relevant axiom analysis. This means that axioms
+    relevant to some function in `P` (but not in `Q`) may be removed. This is
+    sound, but may yield unknown results from the solver.
+  -/
+  | Aggressive
+  /--
+   Functions in both `P` and `Q` of a goal `P ==> Q` will be considered for
+   relevant axiom analysis.
+  -/
+  | Precise
+  /-- Do not prune any axioms. -/
+  | Off
+  deriving Repr, DecidableEq, Inhabited
+
 structure Options where
   verbose : Bool
   parseOnly : Bool
   typeCheckOnly : Bool
   checkOnly : Bool
   stopOnFirstError : Bool
-  removeIrrelevantAxioms : Bool
+  removeIrrelevantAxioms : IrrelevantAxiomsMode
   /-- Solver time limit in seconds -/
   solverTimeout : Nat
 
@@ -20,7 +81,7 @@ def Options.default : Options := {
   typeCheckOnly := false,
   checkOnly := false,
   stopOnFirstError := false,
-  removeIrrelevantAxioms := false,
+  removeIrrelevantAxioms := IrrelevantAxiomsMode.Off,
   solverTimeout := 10
 }
 

Strata/Languages/Boogie/Verifier.lean

@@ -225,6 +225,12 @@ def dischargeObligation
   | .error e => return .error e
   | .ok result => return .ok (result, estate)
 
+private def List.fromMarker (xs : List (String × α)) (marker : String) :
+    List (String × α) :=
+  match xs.dropWhile (fun x => x.fst ≠ marker) with
+  | [] => xs
+  | _ :: ys => ys
+
 def verifySingleEnv (smtsolver : String) (pE : Program × Env) (options : Options) :
     EIO Format VCResults := do
   let (p, E) := pE
@@ -254,19 +260,33 @@ def verifySingleEnv (smtsolver : String) (pE : Program × Env) (options : Option
         results := results.push { obligation, result := .sat .empty, verbose := options.verbose }
         if options.stopOnFirstError then break
       let obligation :=
-      if options.removeIrrelevantAxioms then
-        -- We attempt to prune the path conditions by excluding all irrelevant
-        -- axioms w.r.t. the consequent to reduce the size of the proof
-        -- obligation.
-        let cg := Program.toFunctionCG p
-        let fns := obligation.obligation.getOps.map BoogieIdent.toPretty
-        let relevant_fns := (fns ++ (CallGraph.getAllCalleesClosure cg fns)).dedup
-
-        let irrelevant_axs := Program.getIrrelevantAxioms p relevant_fns
-        let new_assumptions := Imperative.PathConditions.removeByNames obligation.assumptions irrelevant_axs
-        { obligation with assumptions := new_assumptions }
-      else
-        obligation
+        match options.removeIrrelevantAxioms with
+        | .Off => obligation
+        | irrelvantAxMode =>
+          -- We attempt to prune the path conditions by excluding all irrelevant
+          -- axioms to reduce the size of the proof obligation and brittleness due
+          -- to quantifiers.
+          let consequent_fns := obligation.obligation.getOps.map BoogieIdent.toPretty
+          let relevant_fns :=
+            if irrelvantAxMode == IrrelevantAxiomsMode.Aggressive then
+              -- Do not consider functions in the antedent.
+              consequent_fns
+            else
+            -- (HACK) Special marker to grab functions from the VC's assumptions,
+            -- and not from an ever-present prelude. After all, the goal is to
+            -- minimize axioms in this prelude.
+            let non_prelude_assumptions := List.fromMarker obligation.assumptions.flatten "__end_of_prelude_marker"
+            let assumption_fns := non_prelude_assumptions.flatMap (fun a => a.snd.getOps.map BoogieIdent.toPretty)
+            (consequent_fns ++ assumption_fns).dedup
+          let irrelevant_axs := Program.getIrrelevantAxioms p relevant_fns
+          let new_assumptions := Imperative.PathConditions.removeByNames obligation.assumptions irrelevant_axs
+          let new_obligation := ({ obligation with assumptions := new_assumptions } : ProofObligation Expression)
+          if options.verbose then
+            dbg_trace f!"Pruned Proof Obligation:"
+            dbg_trace f!"{format new_obligation}"
+            new_obligation
+          else
+            new_obligation
       -- At this point, we solely rely on the SMT backend.
       let maybeTerms := ProofObligation.toSMTTerms E obligation
       match maybeTerms with

Strata/Languages/Python/BoogiePrelude.lean

@@ -551,6 +551,8 @@ spec {
   assume [assume_maybe_except_none]: (ExceptOrNone_tag(maybe_except) == EN_NONE_TAG);
 };
 
+axiom [__end_of_prelude_marker]: (true);
+
 #end
 
 def Boogie.prelude : Boogie.Program :=

StrataMain.lean

@@ -207,7 +207,7 @@ def pyAnalyzeCommand : Command where
       IO.print newPgm
     let solverName : String := "Strata/Languages/Python/z3_parallel.py"
     let vcResults ← EIO.toIO (fun f => IO.Error.userError (toString f))
-                        (Boogie.verify solverName newPgm { Options.default with stopOnFirstError := false, verbose, removeIrrelevantAxioms := true }
+                        (Boogie.verify solverName newPgm { Options.default with stopOnFirstError := false, verbose, removeIrrelevantAxioms := .Off }
                                                    (moreFns := Strata.Python.ReFactory))
     let mut s := ""
     for vcResult in vcResults do

StrataTest/Languages/Boogie/Examples/RemoveIrrelevantAxioms.lean

@@ -9,7 +9,7 @@ import Strata.Languages.Boogie.Verifier
 ---------------------------------------------------------------------
 namespace Strata
 
-def irrelevantAxiomsTestPgm : Strata.Program :=
+def irrelevantAxiomsTestPgm1 : Strata.Program :=
 #strata
 program Boogie;
 type StrataHeap;
@@ -175,7 +175,7 @@ Obligation: assert_11
 Result: failed
 -/
 #guard_msgs in
-#eval verify "z3" irrelevantAxiomsTestPgm Inhabited.default {Options.quiet with removeIrrelevantAxioms := true}
+#eval verify "z3" irrelevantAxiomsTestPgm1 Inhabited.default {Options.quiet with removeIrrelevantAxioms := .Aggressive}
 
 ---------------------------------------------------------------------
 
@@ -269,6 +269,66 @@ Obligation: assert_11
 Result: unknown
 -/
 #guard_msgs in
-#eval verify "z3" irrelevantAxiomsTestPgm Inhabited.default {Options.quiet with removeIrrelevantAxioms := false}
+#eval verify "z3" irrelevantAxiomsTestPgm1 Inhabited.default {Options.quiet with removeIrrelevantAxioms := .Precise}
+-- Note: Precise irrelevant axiom removal performs just like no axiom removal in
+-- this case.
+
+---------------------------------------------------------------------
+
+def irrelevantAxiomsTestPgm2 : Strata.Program :=
+#strata
+program Boogie;
+
+function f(x : int) : bool;
+function g(x : int) : bool;
+function h(x : int) : bool;
+
+function f2(x : int) : bool { f(x) }
+function fh(x : int) : bool { f2(x) || h(x) }
+
+function h2(x : int) : bool { h(x) }
+
+axiom [f_eq_g]: (forall x : int :: f(x) == g(x));
+axiom [g_eq]: (forall x : int :: g(x) == false);
+axiom [h_eq]: (forall x : int :: h(x) == false);
+axiom [h2_eq]: (forall x : int :: h2(x) == false);
+
+#end
+
+-- Note `g_eq` is detected as relevant for `f` because `g_eq` contains `g`,
+-- which is relevant to axiom `f_eq_g`, which is also relevant to `f`.
+/-- info: ["h_eq", "h2_eq"] -/
+#guard_msgs in
+#eval let (program, _) := Boogie.getProgram irrelevantAxiomsTestPgm2
+      Boogie.Program.getIrrelevantAxioms program ["f"]
+
+/-- info: ["h_eq", "h2_eq"] -/
+#guard_msgs in
+#eval let (program, _) := Boogie.getProgram irrelevantAxiomsTestPgm2
+      Boogie.Program.getIrrelevantAxioms program ["g"]
+
+-- Note `h2_eq` is detected as relevant for `h` because `h2` is a caller of `h`.
+/-- info: ["f_eq_g", "g_eq"] -/
+#guard_msgs in
+#eval let (program, _) := Boogie.getProgram irrelevantAxiomsTestPgm2
+      Boogie.Program.getIrrelevantAxioms program ["h"]
+
+-- Note `h_eq` is detected as relevant for `h2` because `h` is a callee of `h2`.
+/-- info: ["f_eq_g", "g_eq"] -/
+#guard_msgs in
+#eval let (program, _) := Boogie.getProgram irrelevantAxiomsTestPgm2
+      Boogie.Program.getIrrelevantAxioms program ["h2"]
+
+-- Similarly, `f2`'s callee, `f` is considered in the irrelevant axiom
+-- computation.
+/-- info: ["h_eq", "h2_eq"] -/
+#guard_msgs in
+#eval let (program, _) := Boogie.getProgram irrelevantAxiomsTestPgm2
+      Boogie.Program.getIrrelevantAxioms program ["f2"]
+
+/-- info: [] -/
+#guard_msgs in
+#eval let (program, _) := Boogie.getProgram irrelevantAxiomsTestPgm2
+      Boogie.Program.getIrrelevantAxioms program ["fh"]
 
 ---------------------------------------------------------------------

StrataTest/Languages/Python/expected/test_datetime.expected

@@ -13,11 +13,10 @@ assert_opt_name_none_or_bar: verified
 
 ensures_maybe_except_none: verified
 
-py_assertion: unknown
-
 py_assertion: verified
 
+py_assertion: unknown
+
 py_assertion: verified
 
-py_assertion: failed
-CEx: 
+py_assertion: unknown