From 4f2e9e504878d290b0d963dad7a06aa283d5f1f9 Mon Sep 17 00:00:00 2001
From: Levent Erkok <erkokl@gmail.com>
Date: Wed, 3 Jan 2024 11:07:15 -0800
Subject: [PATCH] Add invariant generation example

---
 CHANGES.md                                    |   3 +
 .../SBV/Examples/ProofTools/AddHorn.hs        | 100 ++++++++++++++++++
 sbv.cabal                                     |   1 +
 3 files changed, 104 insertions(+)
 create mode 100644 Documentation/SBV/Examples/ProofTools/AddHorn.hs

diff --git a/CHANGES.md b/CHANGES.md
index 4d71df869..95cb97d7c 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -20,6 +20,9 @@
 
   * Added `Documentation.SBV.Examples.Puzzles.Newspaper`, another puzzle example.
 
+  * Added `Documentation.SBV.Examples.ProofTools.AddHorn`, demonstrating the use of the horn-clause solver for
+    invariant generation.
+
   * Add 'sbv2smt', which renders the given sbv definition as an SMTLib definition. Mainly useful for debugging purposes.
     It can render both ground definitions and functions, and the latter can be handy in producing SMTLib functions to
     be used in other settings.
diff --git a/Documentation/SBV/Examples/ProofTools/AddHorn.hs b/Documentation/SBV/Examples/ProofTools/AddHorn.hs
new file mode 100644
index 000000000..06dd66099
--- /dev/null
+++ b/Documentation/SBV/Examples/ProofTools/AddHorn.hs
@@ -0,0 +1,100 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module    : Documentation.SBV.Examples.ProofTools.AddHorn
+-- Copyright : (c) Levent Erkok
+-- License   : BSD3
+-- Maintainer: erkokl@gmail.com
+-- Stability : experimental
+--
+-- Example of invariant generation for a simple addition algorithm:
+--
+-- @
+--    z = x
+--    i = 0
+--    assume y > 0
+--
+--    while (i < y)
+--       z = z + 1
+--       i = i + 1
+--
+--   assert z == x + y
+-- @
+--
+-- We use the Horn solver to calculate the invariant and then show that it
+-- indeed is a sufficient invariant to establish correctness.
+-----------------------------------------------------------------------------
+
+{-# LANGUAGE DataKinds #-}
+
+{-# OPTIONS_GHC -Wall -Werror #-}
+
+module Documentation.SBV.Examples.ProofTools.AddHorn where
+
+import Data.SBV
+
+-- | Helper type synonym for the invariant.
+type Inv = (SInteger, SInteger, SInteger, SInteger) -> SBool
+
+-- | Helper type synonym for verification conditions.
+type VC = Forall "x" Integer -> Forall "y" Integer -> Forall "z" Integer -> Forall "i" Integer -> SBool
+
+-- | Helper for turning an invariant predicate to a boolean.
+quantify :: Inv -> VC
+quantify f = \(Forall x) (Forall y) (Forall z) (Forall i) -> f (x, y, z, i)
+
+-- | First verification condition: Before the loop starts, invariant must hold:
+--
+-- \(z = x \land i = 0 \land y > 0 \Rightarrow inv (x, y, z, i)\)
+vc1 :: Inv -> VC
+vc1 inv = quantify $ \(x, y, z, i) -> z .== x .&& i .== 0 .&& y .> 0 .=> inv (x, y, z, i)
+
+-- | Second verification condition: If the loop body executes, invariant must still hold at the end:
+--
+-- \(inv (x, y, z, i) \land i < y \Rightarrow inv (x, y, z+1, i+1)\)
+vc2 :: Inv -> VC
+vc2 inv = quantify $ \(x, y, z, i) -> inv (x, y, z, i) .&& i .< y .=> inv (x, y, z+1, i+1)
+
+-- | Third verification condition: Once the loop exits, invariant and the negation of the loop condition
+-- must establish the final assertion:
+--
+-- \(inv (x, y, z, i) \land i \geq y \Rightarrow z == x + y\)
+vc3 :: Inv -> VC
+vc3 inv = quantify $ \(x, y, z, i) -> inv (x, y, z, i) .&& i .>= y .=> z .== x + y
+
+-- | Synthesize the invariant. We use an uninterpreted function for the SMT solver to synthesize. We get:
+--
+-- >>> synthesize
+-- Satisfiable. Model:
+--   invariant :: (Integer, Integer, Integer, Integer) -> Bool
+--   invariant (x, y, z, i) = x + (-z) + i > (-1) && x + (-z) + i < 1 && x + y + (-z) > (-1)
+--
+-- This is a bit hard to read, but you can convince yourself it is equivalent to @x + i .== z .&& x + y .>= z@:
+--
+-- >>> let f (x, y, z, i) = x + (-z) + i .> (-1) .&& x + (-z) + i .< 1 .&& x + y + (-z) .> (-1)
+-- >>> let g (x, y, z, i) = x + i .== z .&& x + y .>= z
+-- >>> f === (g :: Inv)
+-- Q.E.D.
+synthesize :: IO SatResult
+synthesize = sat vcs
+  where invariant :: Inv
+        invariant = uninterpretWithArgs "invariant" ["x", "y", "z", "i"]
+
+        vcs :: ConstraintSet
+        vcs = do setLogic $ CustomLogic "HORN"
+                 constrain $ vc1 invariant
+                 constrain $ vc2 invariant
+                 constrain $ vc3 invariant
+
+-- | Verify that the synthesized function does indeed work. To do so, we simply prove that the invariant found satisfies all the vcs:
+--
+-- >>> verify
+-- Q.E.D.
+verify :: IO ThmResult
+verify = prove vcs
+  where invariant :: Inv
+        invariant (x, y, z, i) = x + (-z) + i .> (-1) .&& x + (-z) + i .< 1 .&& x + y + (-z) .> (-1)
+
+        vcs :: SBool
+        vcs =   quantifiedBool (vc1 invariant)
+            .&& quantifiedBool (vc3 invariant)
+            .&& quantifiedBool (vc3 invariant)
diff --git a/sbv.cabal b/sbv.cabal
index 4b36ac8da..6c74317c1 100644
--- a/sbv.cabal
+++ b/sbv.cabal
@@ -174,6 +174,7 @@ Library
                   , Documentation.SBV.Examples.Optimization.LinearOpt
                   , Documentation.SBV.Examples.Optimization.Production
                   , Documentation.SBV.Examples.Optimization.VM
+                  , Documentation.SBV.Examples.ProofTools.AddHorn
                   , Documentation.SBV.Examples.ProofTools.BMC
                   , Documentation.SBV.Examples.ProofTools.Fibonacci
                   , Documentation.SBV.Examples.ProofTools.Strengthen