-----------------------------------------------------------------------------
-- |
-- Module    : Documentation.SBV.Examples.KnuckleDragger.BinarySearch
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Proving binary search correct
-----------------------------------------------------------------------------

{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE TypeAbstractions    #-}
{-# LANGUAGE TypeApplications    #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.KnuckleDragger.BinarySearch where

import Prelude hiding (null, length, (!!), drop, take, tail, elem, notElem)

import Data.SBV
import Data.SBV.Maybe
import Data.SBV.Tools.KnuckleDragger

-- * Binary search

-- | We will work with arrays containing integers, indexed by integers. Note that since SMTLib arrays
-- are indexed by their entire domain, we explicitly take a lower/upper bounds as parameters, which fits well
-- with the binary search algorithm.
type Arr = SArray Integer Integer

-- | Bounds: This is the focus into the array; both indexes are inclusive.
type Idx = (SInteger, SInteger)

-- | Encode binary search in a functional style.
bsearch :: Arr -> Idx -> SInteger -> SMaybe Integer
bsearch :: Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
array (SInteger
low, SInteger
high) = Arr -> SInteger -> SInteger -> SInteger -> SMaybe Integer
f Arr
array SInteger
low SInteger
high
  where f :: Arr -> SInteger -> SInteger -> SInteger -> SMaybe Integer
f = String
-> (Arr -> SInteger -> SInteger -> SInteger -> SMaybe Integer)
-> Arr
-> SInteger
-> SInteger
-> SInteger
-> SMaybe Integer
forall a. (SMTDefinable a, Lambda Symbolic a) => String -> a -> a
smtFunction String
"bsearch" ((Arr -> SInteger -> SInteger -> SInteger -> SMaybe Integer)
 -> Arr -> SInteger -> SInteger -> SInteger -> SMaybe Integer)
-> (Arr -> SInteger -> SInteger -> SInteger -> SMaybe Integer)
-> Arr
-> SInteger
-> SInteger
-> SInteger
-> SMaybe Integer
forall a b. (a -> b) -> a -> b
$ \Arr
arr SInteger
lo SInteger
hi SInteger
x ->
               let mid :: SInteger
mid  = (SInteger
lo SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
hi) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2
                   xmid :: SInteger
xmid = Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SInteger
mid
               in SBool -> SMaybe Integer -> SMaybe Integer -> SMaybe Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
hi)
                      SMaybe Integer
forall a. SymVal a => SMaybe a
sNothing
                      (SBool -> SMaybe Integer -> SMaybe Integer -> SMaybe Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x)
                           (SInteger -> SMaybe Integer
forall a. SymVal a => SBV a -> SMaybe a
sJust SInteger
mid)
                           (SBool -> SMaybe Integer -> SMaybe Integer -> SMaybe Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
x)
                                (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1, SInteger
hi)    SInteger
x)
                                (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo,    SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1) SInteger
x)))

-- * Correctness proof

-- | A predicate testing whether a given array is non-decreasing in the given range
nonDecreasing :: Arr -> Idx -> SBool
nonDecreasing :: Arr -> Idx -> SBool
nonDecreasing Arr
arr (SInteger
low, SInteger
high) = (Forall "i" Integer -> Forall "j" Integer -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool ((Forall "i" Integer -> Forall "j" Integer -> SBool) -> SBool)
-> (Forall "i" Integer -> Forall "j" Integer -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$
    \(Forall @"i" SInteger
i) (Forall @"j" SInteger
j) -> SInteger
low SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
i SBool -> SBool -> SBool
.&& SInteger
i SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
j SBool -> SBool -> SBool
.&& SInteger
j SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
high SBool -> SBool -> SBool
.=> Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SInteger
i SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SInteger
j

-- | A predicate testing whether an element is in the array within the given bounds
inArray :: Arr -> Idx -> SInteger -> SBool
inArray :: Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
low, SInteger
high) SInteger
elt = (Exists "i" Integer -> SBool) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool ((Exists "i" Integer -> SBool) -> SBool)
-> (Exists "i" Integer -> SBool) -> SBool
forall a b. (a -> b) -> a -> b
$ \(Exists @"i" SInteger
i) -> SInteger
low SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
i SBool -> SBool -> SBool
.&& SInteger
i SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
high SBool -> SBool -> SBool
.&& Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SInteger
i SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
elt

-- | Correctness of binary search.
--
-- We have:
--
-- >>> correctness
-- Lemma: notInRange                                 Q.E.D.
-- Lemma: inRangeHigh                                Q.E.D.
-- Lemma: inRangeLow                                 Q.E.D.
-- Lemma: nonDecreasing                              Q.E.D.
-- Inductive lemma (strong): bsearchAbsent
--   Step: Measure is non-negative                   Q.E.D.
--   Step: 1 (unfold bsearch)                        Q.E.D.
--   Step: 2 (push isNothing down, simplify)         Q.E.D.
--   Step: 3 (2 way case split)
--     Step: 3.1                                     Q.E.D.
--     Step: 3.2.1                                   Q.E.D.
--     Step: 3.2.2                                   Q.E.D.
--     Step: 3.2.3                                   Q.E.D.
--     Step: 3.2.4                                   Q.E.D.
--     Step: 3.2.5 (simplify)                        Q.E.D.
--     Step: 3.Completeness                          Q.E.D.
--   Result:                                         Q.E.D.
-- Inductive lemma (strong): bsearchPresent
--   Step: Measure is non-negative                   Q.E.D.
--   Step: 1 (unfold bsearch)                        Q.E.D.
--   Step: 2 (simplify)                              Q.E.D.
--   Step: 3 (3 way case split)
--     Step: 3.1                                     Q.E.D.
--     Step: 3.2                                     Q.E.D.
--     Step: 3.3.1                                   Q.E.D.
--     Step: 3.3.2 (3 way case split)
--       Step: 3.3.2.1                               Q.E.D.
--       Step: 3.3.2.2.1                             Q.E.D.
--       Step: 3.3.2.2.2                             Q.E.D.
--       Step: 3.3.2.3.1                             Q.E.D.
--       Step: 3.3.2.3.2                             Q.E.D.
--       Step: 3.3.2.Completeness                    Q.E.D.
--     Step: 3.Completeness                          Q.E.D.
--   Result:                                         Q.E.D.
-- Lemma: bsearchCorrect
--   Step: 1 (2 way case split)
--     Step: 1.1.1                                   Q.E.D.
--     Step: 1.1.2                                   Q.E.D.
--     Step: 1.2.1                                   Q.E.D.
--     Step: 1.2.2                                   Q.E.D.
--     Step: 1.Completeness                          Q.E.D.
--   Result:                                         Q.E.D.
-- [Proven] bsearchCorrect
correctness :: IO Proof
correctness :: IO Proof
correctness = SMTConfig -> KD Proof -> IO Proof
forall a. SMTConfig -> KD a -> IO a
runKDWith SMTConfig
z3{kdOptions = (kdOptions z3) { ribbonLength = 50 }} (KD Proof -> IO Proof) -> KD Proof -> IO Proof
forall a b. (a -> b) -> a -> b
$ do

  -- Helper: if a value is not in a range, then it isn't in any subrange of it:
  notInRange <- String
-> (Forall "arr" (ArrayModel Integer Integer)
    -> Forall "lo" Integer
    -> Forall "hi" Integer
    -> Forall "m" Integer
    -> Forall "x" Integer
    -> SBool)
-> [Proof]
-> KD Proof
forall a. Proposition a => String -> a -> [Proof] -> KD Proof
lemma String
"notInRange"
                           (\(Forall @"arr" Arr
arr) (Forall @"lo" SInteger
lo) (Forall @"hi" SInteger
hi) (Forall @"m" SInteger
md) (Forall @"x" SInteger
x)
                               ->  SBool -> SBool
sNot (Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
lo, SInteger
hi) SInteger
x) SBool -> SBool -> SBool
.&& SInteger
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
md SBool -> SBool -> SBool
.&& SInteger
md SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
hi
                               SBool -> SBool -> SBool
.=> SBool -> SBool
sNot (Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
lo, SInteger
md) SInteger
x) SBool -> SBool -> SBool
.&& SBool -> SBool
sNot (Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
md, SInteger
hi) SInteger
x))
                           []

  -- Helper: if a value is in a range of a nonDecreasing array, and if its value is larger than a given mid point, then it's in the higher part
  inRangeHigh <- lemma "inRangeHigh"
                       (\(Forall @"arr" Arr
arr) (Forall @"lo" SInteger
lo) (Forall @"hi" SInteger
hi) (Forall @"m" SInteger
md) (Forall @"x" SInteger
x)
                           ->  Arr -> Idx -> SBool
nonDecreasing Arr
arr (SInteger
lo, SInteger
hi) SBool -> SBool -> SBool
.&& Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
lo, SInteger
hi) SInteger
x SBool -> SBool -> SBool
.&& SInteger
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
md SBool -> SBool -> SBool
.&& SInteger
md SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
hi SBool -> SBool -> SBool
.&& SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SInteger
md
                           SBool -> SBool -> SBool
.=> Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
mdSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1, SInteger
hi) SInteger
x)
                       []

  -- Helper: if a value is in a range of a nonDecreasing array, and if its value is lower than a given mid point, then it's in the lowr part
  inRangeLow  <- lemma "inRangeLow"
                       (\(Forall @"arr" Arr
arr) (Forall @"lo" SInteger
lo) (Forall @"hi" SInteger
hi) (Forall @"m" SInteger
md) (Forall @"x" SInteger
x)
                           ->  Arr -> Idx -> SBool
nonDecreasing Arr
arr (SInteger
lo, SInteger
hi) SBool -> SBool -> SBool
.&& Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
lo, SInteger
hi) SInteger
x SBool -> SBool -> SBool
.&& SInteger
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
md SBool -> SBool -> SBool
.&& SInteger
md SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
hi SBool -> SBool -> SBool
.&& SInteger
x SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SInteger
md
                           SBool -> SBool -> SBool
.=> Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
lo, SInteger
mdSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1) SInteger
x)
                       []

  -- Helper: if an array is nonDecreasing, then its parts are also non-decreasing when cut in any middle point
  nonDecreasingInRange <- lemma "nonDecreasing"
                                (\(Forall @"arr" Arr
arr) (Forall @"lo" SInteger
lo) (Forall @"hi" SInteger
hi) (Forall @"m" SInteger
md)
                                    ->  Arr -> Idx -> SBool
nonDecreasing Arr
arr (SInteger
lo, SInteger
hi) SBool -> SBool -> SBool
.&& SInteger
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
md SBool -> SBool -> SBool
.&& SInteger
md SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
hi
                                    SBool -> SBool -> SBool
.=> Arr -> Idx -> SBool
nonDecreasing Arr
arr (SInteger
lo, SInteger
md) SBool -> SBool -> SBool
.&& Arr -> Idx -> SBool
nonDecreasing Arr
arr (SInteger
md, SInteger
hi))
                                []

  -- Prove the case when the target is not in the array
  bsearchAbsent <- sInduct "bsearchAbsent"
        (\(Forall @"arr" Arr
arr) (Forall @"lo" SInteger
lo) (Forall @"hi" SInteger
hi) (Forall @"x" SInteger
x) ->
            Arr -> Idx -> SBool
nonDecreasing Arr
arr (SInteger
lo, SInteger
hi) SBool -> SBool -> SBool
.&& SBool -> SBool
sNot (Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
lo, SInteger
hi) SInteger
x) SBool -> SBool -> SBool
.=> SMaybe Integer -> SBool
forall a. SymVal a => SMaybe a -> SBool
isNothing (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo, SInteger
hi) SInteger
x))
        (\(Arr
_arr :: Arr) (SInteger
lo :: SInteger) (SInteger
hi :: SInteger) (SInteger
_x :: SInteger) -> SInteger -> SInteger
forall a. Num a => a -> a
abs (SInteger
hi SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
lo SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1)) $
        \Proof
ih Arr
arr SInteger
lo SInteger
hi SInteger
x ->
              [Arr -> Idx -> SBool
nonDecreasing Arr
arr (SInteger
lo, SInteger
hi), SBool -> SBool
sNot (Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
lo, SInteger
hi) SInteger
x)]
           [SBool] -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SMaybe Integer -> SBool
forall a. SymVal a => SMaybe a -> SBool
isNothing (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo, SInteger
hi) SInteger
x)
           SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"unfold bsearch"
           KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: let mid :: SInteger
mid  = (SInteger
lo SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
hi) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2
                  xmid :: SInteger
xmid = Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SInteger
mid
           in SMaybe Integer -> SBool
forall a. SymVal a => SMaybe a -> SBool
isNothing (SBool -> SMaybe Integer -> SMaybe Integer -> SMaybe Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
hi)
                             SMaybe Integer
forall a. SymVal a => SMaybe a
sNothing
                             (SBool -> SMaybe Integer -> SMaybe Integer -> SMaybe Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x)
                                  (SInteger -> SMaybe Integer
forall a. SymVal a => SBV a -> SMaybe a
sJust SInteger
mid)
                                  (SBool -> SMaybe Integer -> SMaybe Integer -> SMaybe Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
x)
                                       (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1, SInteger
hi)    SInteger
x)
                                       (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo,    SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1) SInteger
x))))
           SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"push isNothing down, simplify"
           KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
hi)
                  SBool
sTrue
                  (SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x)
                       SBool
sFalse
                       (SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
x)
                            (SMaybe Integer -> SBool
forall a. SymVal a => SMaybe a -> SBool
isNothing (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1, SInteger
hi)    SInteger
x))
                            (SMaybe Integer -> SBool
forall a. SymVal a => SMaybe a -> SBool
isNothing (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo,    SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1) SInteger
x))))
           SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, KDProofRaw SBool)] -> KDProofRaw SBool
forall a. [(SBool, KDProofRaw a)] -> KDProofRaw a
cases [ SInteger
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
hi  SBool -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
==> KDProofRaw SBool
forall a. Trivial a => a
trivial
                    , SInteger
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<= SInteger
hi SBool -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
==> SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x)
                                        SBool
sFalse
                                        (SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
x)
                                             (SMaybe Integer -> SBool
forall a. SymVal a => SMaybe a -> SBool
isNothing (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1, SInteger
hi)    SInteger
x))
                                             (SMaybe Integer -> SBool
forall a. SymVal a => SMaybe a -> SBool
isNothing (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo,    SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1) SInteger
x)))
                                 SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: let inst1 :: SBV a
-> SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "m" a, Inst "x" Integer)
inst1 SBV a
l SBV a
h SBV a
m = (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"arr" Arr
arr, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"lo" SBV a
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"hi" SBV a
h, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV a
m, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SInteger
x)
                                        inst2 :: SBV a
-> SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "m" a)
inst2 SBV a
l SBV a
h SBV a
m = (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"arr" Arr
arr, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"lo" SBV a
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"hi" SBV a
h, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV a
m             )
                                        inst3 :: SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "x" Integer)
inst3 SBV a
l SBV a
h   = (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"arr" Arr
arr, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"lo" SBV a
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"hi" SBV a
h,              forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SInteger
x)
                                 in SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
x)
                                        (SMaybe Integer -> SBool
forall a. SymVal a => SMaybe a -> SBool
isNothing (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1, SInteger
hi)    SInteger
x))
                                        (SMaybe Integer -> SBool
forall a. SymVal a => SMaybe a -> SBool
isNothing (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo,    SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1) SInteger
x))
                                 SBool -> [Proof] -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? [ Proof
notInRange           Proof
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "m" Integer, Inst "x" Integer)
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` SInteger
-> SInteger
-> SInteger
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "m" Integer, Inst "x" Integer)
forall {a} {a} {a}.
SBV a
-> SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "m" a, Inst "x" Integer)
inst1 SInteger
lo      SInteger
hi (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)
                                    , Proof
nonDecreasingInRange Proof
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "m" Integer)
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` SInteger
-> SInteger
-> SInteger
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "m" Integer)
forall {a} {a} {a}.
SBV a
-> SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "m" a)
inst2 SInteger
lo      SInteger
hi (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)
                                    , Proof
ih                   Proof
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "x" Integer)
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` SInteger
-> SInteger
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "x" Integer)
forall {a} {a}.
SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "x" Integer)
inst3 (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger
hi
                                    ]
                                 KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
x)
                                        SBool
sTrue
                                        (SMaybe Integer -> SBool
forall a. SymVal a => SMaybe a -> SBool
isNothing (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo,    SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1) SInteger
x))
                                 SBool -> [Proof] -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? [ Proof
notInRange           Proof
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "m" Integer, Inst "x" Integer)
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` SInteger
-> SInteger
-> SInteger
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "m" Integer, Inst "x" Integer)
forall {a} {a} {a}.
SBV a
-> SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "m" a, Inst "x" Integer)
inst1 SInteger
lo SInteger
hi      (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1)
                                    , Proof
nonDecreasingInRange Proof
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "m" Integer)
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` SInteger
-> SInteger
-> SInteger
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "m" Integer)
forall {a} {a} {a}.
SBV a
-> SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "m" a)
inst2 SInteger
lo SInteger
hi      (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1)
                                    , Proof
ih                   Proof
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "x" Integer)
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` SInteger
-> SInteger
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "x" Integer)
forall {a} {a}.
SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "x" Integer)
inst3 SInteger
lo (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1)
                                    ]
                                 KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
x) SBool
sTrue SBool
sTrue
                                 SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"simplify"
                                 KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                 SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
KDProofRaw SBool
forall a. KDProofRaw a
qed
                    ]

  -- Prove the case when the target is in the array
  bsearchPresent <- sInduct "bsearchPresent"
        (\(Forall @"arr" Arr
arr) (Forall @"lo" SInteger
lo) (Forall @"hi" SInteger
hi) (Forall @"x" SInteger
x) ->
            Arr -> Idx -> SBool
nonDecreasing Arr
arr (SInteger
lo, SInteger
hi) SBool -> SBool -> SBool
.&& Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
lo, SInteger
hi) SInteger
x SBool -> SBool -> SBool
.=> Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SMaybe Integer -> SInteger
forall a. SymVal a => SMaybe a -> SBV a
fromJust (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo, SInteger
hi) SInteger
x) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x)
        (\(Arr
_arr :: Arr) (SInteger
lo :: SInteger) (SInteger
hi :: SInteger) (SInteger
_x :: SInteger) -> SInteger -> SInteger
forall a. Num a => a -> a
abs (SInteger
hi SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
- SInteger
lo SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
1)) $
        \Proof
ih Arr
arr SInteger
lo SInteger
hi SInteger
x ->
             [Arr -> Idx -> SBool
nonDecreasing Arr
arr (SInteger
lo, SInteger
hi), Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
lo, SInteger
hi) SInteger
x]
          [SBool] -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SMaybe Integer -> SInteger
forall a. SymVal a => SMaybe a -> SBV a
fromJust (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo, SInteger
hi) SInteger
x)
          SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"unfold bsearch"
          KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: let mid :: SInteger
mid  = (SInteger
lo SInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+ SInteger
hi) SInteger -> SInteger -> SInteger
`sEDiv` SInteger
2
                 xmid :: SInteger
xmid = Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SInteger
mid
          in SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SMaybe Integer -> SInteger
forall a. SymVal a => SMaybe a -> SBV a
fromJust (SBool -> SMaybe Integer -> SMaybe Integer -> SMaybe Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
hi)
                                                 SMaybe Integer
forall a. SymVal a => SMaybe a
sNothing
                                                 (SBool -> SMaybe Integer -> SMaybe Integer -> SMaybe Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x)
                                                      (SInteger -> SMaybe Integer
forall a. SymVal a => SBV a -> SMaybe a
sJust SInteger
mid)
                                                      (SBool -> SMaybe Integer -> SMaybe Integer -> SMaybe Integer
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
x)
                                                           (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1, SInteger
hi)    SInteger
x)
                                                           (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo,    SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1) SInteger
x))))
          SBool -> String -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? String
"simplify"
          KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
hi)
                 (SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SMaybe Integer -> SInteger
forall a. SymVal a => SMaybe a -> SBV a
fromJust SMaybe Integer
forall a. SymVal a => SMaybe a
sNothing)
                 (SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x)
                      (SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SInteger
mid)
                      (SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
x)
                           (SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SMaybe Integer -> SInteger
forall a. SymVal a => SMaybe a -> SBV a
fromJust (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1, SInteger
hi)    SInteger
x))
                           (SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SMaybe Integer -> SInteger
forall a. SymVal a => SMaybe a -> SBV a
fromJust (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo,    SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1) SInteger
x))))
          SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, KDProofRaw SBool)] -> KDProofRaw SBool
forall a. [(SBool, KDProofRaw a)] -> KDProofRaw a
cases [ SInteger
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.>  SInteger
hi SBool -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
==> KDProofRaw SBool
forall a. Trivial a => a
trivial
                   , SInteger
lo SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
hi SBool -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
==> KDProofRaw SBool
forall a. Trivial a => a
trivial
                   , SInteger
lo SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.<  SInteger
hi SBool -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
==> SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x)
                                       (SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SInteger
mid)
                                       (SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (SInteger
xmid SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
x)
                                            (SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SMaybe Integer -> SInteger
forall a. SymVal a => SMaybe a -> SBV a
fromJust (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1, SInteger
hi)    SInteger
x))
                                            (SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SMaybe Integer -> SInteger
forall a. SymVal a => SMaybe a -> SBV a
fromJust (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo,    SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1) SInteger
x)))
                                SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: let inst1 :: SBV a
-> SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "m" a, Inst "x" Integer)
inst1 SBV a
l SBV a
h SBV a
m = (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"arr" Arr
arr, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"lo" SBV a
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"hi" SBV a
h, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV a
m, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SInteger
x)
                                       inst2 :: SBV a
-> SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "m" a)
inst2 SBV a
l SBV a
h SBV a
m = (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"arr" Arr
arr, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"lo" SBV a
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"hi" SBV a
h, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"m" SBV a
m             )
                                       inst3 :: SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "x" Integer)
inst3 SBV a
l SBV a
h   = (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"arr" Arr
arr, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"lo" SBV a
l, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"hi" SBV a
h,              forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SInteger
x)
                                in [(SBool, KDProofRaw SBool)] -> KDProofRaw SBool
forall a. [(SBool, KDProofRaw a)] -> KDProofRaw a
cases [ SInteger
xmid SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x SBool -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
==> KDProofRaw SBool
forall a. Trivial a => a
trivial
                                         , SInteger
xmid SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.< SInteger
x  SBool -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
==> SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SMaybe Integer -> SInteger
forall a. SymVal a => SMaybe a -> SBV a
fromJust (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1, SInteger
hi)    SInteger
x)
                                                       SBool -> [Proof] -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? [ Proof
inRangeHigh          Proof
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "m" Integer, Inst "x" Integer)
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` SInteger
-> SInteger
-> SInteger
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "m" Integer, Inst "x" Integer)
forall {a} {a} {a}.
SBV a
-> SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "m" a, Inst "x" Integer)
inst1 SInteger
lo      SInteger
hi SInteger
mid
                                                          , Proof
nonDecreasingInRange Proof
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "m" Integer)
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` SInteger
-> SInteger
-> SInteger
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "m" Integer)
forall {a} {a} {a}.
SBV a
-> SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "m" a)
inst2 SInteger
lo      SInteger
hi (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1)
                                                          , Proof
ih                   Proof
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "x" Integer)
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` SInteger
-> SInteger
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "x" Integer)
forall {a} {a}.
SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "x" Integer)
inst3 (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
+SInteger
1) SInteger
hi
                                                          ]
                                                       KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                                       SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
KDProofRaw SBool
forall a. KDProofRaw a
qed
                                         , SInteger
xmid SInteger -> SInteger -> SBool
forall a. OrdSymbolic a => a -> a -> SBool
.> SInteger
x  SBool -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
==> SInteger
x SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SMaybe Integer -> SInteger
forall a. SymVal a => SMaybe a -> SBV a
fromJust (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo, SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1) SInteger
x)
                                                       SBool -> [Proof] -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? [ Proof
inRangeLow           Proof
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "m" Integer, Inst "x" Integer)
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` SInteger
-> SInteger
-> SInteger
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "m" Integer, Inst "x" Integer)
forall {a} {a} {a}.
SBV a
-> SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "m" a, Inst "x" Integer)
inst1 SInteger
lo SInteger
hi      SInteger
mid
                                                          , Proof
nonDecreasingInRange Proof
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "m" Integer)
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` SInteger
-> SInteger
-> SInteger
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "m" Integer)
forall {a} {a} {a}.
SBV a
-> SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "m" a)
inst2 SInteger
lo SInteger
hi      (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1)
                                                          , Proof
ih                   Proof
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "x" Integer)
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` SInteger
-> SInteger
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "x" Integer)
forall {a} {a}.
SBV a
-> SBV a
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" a,
    Inst "hi" a, Inst "x" Integer)
inst3 SInteger
lo (SInteger
midSInteger -> SInteger -> SInteger
forall a. Num a => a -> a -> a
-SInteger
1)
                                                          ]
                                                       KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                                       SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
KDProofRaw SBool
forall a. KDProofRaw a
qed
                                         ]
                   ]

  calc "bsearchCorrect"
        (\(Forall @"arr" Arr
arr) (Forall @"lo" SInteger
lo) (Forall @"hi" SInteger
hi) (Forall @"x" SInteger
x) ->
            Arr -> Idx -> SBool
nonDecreasing Arr
arr (SInteger
lo, SInteger
hi) SBool -> SBool -> SBool
.=> let res :: SMaybe Integer
res = Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo, SInteger
hi) SInteger
x
                                           in SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
lo, SInteger
hi) SInteger
x)
                                                  (Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SMaybe Integer -> SInteger
forall a. SymVal a => SMaybe a -> SBV a
fromJust SMaybe Integer
res SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x)
                                                  (SMaybe Integer -> SBool
forall a. SymVal a => SMaybe a -> SBool
isNothing SMaybe Integer
res)) $
        \Arr
arr SInteger
lo SInteger
hi SInteger
x -> [Arr -> Idx -> SBool
nonDecreasing Arr
arr (SInteger
lo, SInteger
hi)]
                     [SBool] -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. [SBool] -> KDProofRaw a -> (SBool, KDProofRaw a)
|- let res :: SMaybe Integer
res = Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo, SInteger
hi) SInteger
x
                        in SBool -> SBool -> SBool -> SBool
forall a. Mergeable a => SBool -> a -> a -> a
ite (Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
lo, SInteger
hi) SInteger
x)
                               (Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SMaybe Integer -> SInteger
forall a. SymVal a => SMaybe a -> SBV a
fromJust SMaybe Integer
res SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x)
                               (SMaybe Integer -> SBool
forall a. SymVal a => SMaybe a -> SBool
isNothing SMaybe Integer
res)
                     SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: [(SBool, KDProofRaw SBool)] -> KDProofRaw SBool
forall a. [(SBool, KDProofRaw a)] -> KDProofRaw a
cases [ Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
lo, SInteger
hi) SInteger
x
                                  SBool -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
==> Arr
arr Arr -> SInteger -> SInteger
forall key val.
(Eq key, SymVal key, SymVal val, HasKind val) =>
SArray key val -> SBV key -> SBV val
`readArray` SMaybe Integer -> SInteger
forall a. SymVal a => SMaybe a -> SBV a
fromJust (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo, SInteger
hi) SInteger
x) SInteger -> SInteger -> SBool
forall a. EqSymbolic a => a -> a -> SBool
.== SInteger
x
                                   SBool -> Proof -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
bsearchPresent Proof
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "x" Integer)
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"arr" Arr
arr, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"lo" SInteger
lo, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"hi" SInteger
hi, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SInteger
x)
                                   KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                   SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
KDProofRaw SBool
forall a. KDProofRaw a
qed
                              , SBool -> SBool
sNot (Arr -> Idx -> SInteger -> SBool
inArray Arr
arr (SInteger
lo, SInteger
hi) SInteger
x)
                                  SBool -> KDProofRaw SBool -> (SBool, KDProofRaw SBool)
forall a. SBool -> KDProofRaw a -> (SBool, KDProofRaw a)
==> SMaybe Integer -> SBool
forall a. SymVal a => SMaybe a -> SBool
isNothing (Arr -> Idx -> SInteger -> SMaybe Integer
bsearch Arr
arr (SInteger
lo, SInteger
hi) SInteger
x)
                                   SBool -> Proof -> Hinted SBool
forall a b. HintsTo a b => a -> b -> Hinted a
?? Proof
bsearchAbsent Proof
-> (Inst "arr" (ArrayModel Integer Integer), Inst "lo" Integer,
    Inst "hi" Integer, Inst "x" Integer)
-> Proof
forall a. Instantiatable a => Proof -> a -> Proof
`at` (forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"arr" Arr
arr, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"lo" SInteger
lo, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"hi" SInteger
hi, forall (nm :: Symbol) a. SBV a -> Inst nm a
Inst @"x" SInteger
x)
                                   KDProofRaw SBool
-> ChainsTo (KDProofRaw SBool) -> ChainsTo (KDProofRaw SBool)
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: SBool
sTrue
                                   SBool -> ChainsTo SBool -> ChainsTo SBool
forall a. ChainStep a (ChainsTo a) => a -> ChainsTo a -> ChainsTo a
=: ChainsTo SBool
KDProofRaw SBool
forall a. KDProofRaw a
qed
                              ]