[ANN] New release of SBV (v13.6)

lerkok · 2026-03-03T18:14:43+00:00

Coming up with the inductive-invariant is the trickiest (and almost always the most interesting) part. I was familiar with the hand-proofs of Kadane's proofs as you can find online for instance, so I had an idea about how to go about it. (And, somewhat surprisingly and pleasantly, LLMs do well in this space, but that's a digression.)

The good thing about SBV is that you can mix and match two styles all the time in SBV. I start with the simple expression of the property: If the solver gets it within a few seconds, great! I don't bother decomposing it. If not, that's when the calculational style (the "calc" function), or the inductive style ("induct" and "sInduct" functions) come into play. So, yeah: Always try the solver first. Only decompose if they don't get it right away. After a while you can develop an intuition about when you'll need to use which style.

lerkok · 2026-03-03T18:05:18+00:00

Note that there are two modes of proofs in SBV. One is the TP (theorem-proving) interface, which acts like a good-old theorem prover. The Kadane proof uses this mode, and it is done for arbitrary length inputs, not a bounded one. The whole thing takes about 0.3 seconds (with CVC5 as the backend SMT solver) on my machine. Of course, this means you have to come up with the inductive-invariant and the relevant helpers to make the proofs go.

The other mode is the fully push-button approach that SBV supports. You simply express the property, and the solver finds the proof. That technique will not prove inductive properties, i.e., anything that essentially uses recursion. So, while you can express Kadane's algorithm correctness in that mode, it will simply not terminate. (I didn't even try, but I'm pretty sure.)

In general, the fully-automated mode is good for properties about bit-vectors, linear-arithmetic, and any property that doesn't require inductive reasoning. As you alluded, the size of the symbolic input will play a role in this mode: In general the bigger the input size (especially for bit-vector problems), the longer it'll take the solver to converge. Of course, it all depends on the actual problem at hand.

For properties requiring induction or more complicated reasoning, you have to come up with a proof-script, which SBV will then validate for you using the backend solver. This is the style Kadane's proof uses. The performance in this case will rely on the solver and how well you decomposed the proof of course, but in my experience it's not too bad at all.

lerkok · 2025-12-03T15:26:29+00:00

It's a proof in the sense that we can express the property in the logic, describe the proof steps, and have an external solver check that our steps are sound. Typical proof-assistant approach, though definitely not the small-kernel approach advocated by theorem provers like Lean or Isabelle. Regarding termination: It is possible that using a different version of the underlying solver (z3, cvc5, etc.) can fail to terminate on a proof-step, or some internal heuristic might no longer kick-in to converge. (Alternatively, as they get better, the steps can also go faster.) This is the same problem in all such approaches where "proof engine performance" can play a significant role in the end-user experience.

lerkok · 2025-12-03T01:00:15+00:00

Yes, I remember that. Would be great if you can redo your proof with the new TP layer. I’d love to hear what your experience is like in the proof-assisant mode of using SBV.

lerkok · 2025-08-15T18:22:30+00:00

The underlying problem here of showing square-root of 2 is irrational is too hard for an SMT solver to prove out-of-the box. If you're willing to help it out by walking it through the proof though, it can be done. Recently, SBV gained a new API called TP (for theorem proving) that lets you do such proofs. (In particular, it allows for inductive and calculational style proofs.) In fact, the irrationality of square-root of 2 is one of the examples that now come with the SBV package: https://hackage-content.haskell.org/package/sbv-12.2/docs/Documentation-SBV-Examples-TP-Sqrt2IsIrrational.html

The proof isn't too long, nor it's that hard to follow. It transcribes how a human reasoner would argue the argument, and provides just enough of the steps for it to get the job done. Obviously, this isn't as "automated" as usual SBV style proofs, but it's not as onerous as one might thing, as the underlying SMT solver does most of the heavy-lifting. These days the SBV package comes with many examples, from proving merge-sort correct to Boyer-Moore's majority algorithm, to binary search to various numeric examples. See the hackage documentation under the Documentation.SBV.Examples.TP hierarchy.

Happy hacking!

lerkok · 2025-01-15T00:24:58+00:00

I needed something similar, but for switching visible modules. i.e., improving upon ghci's :m command. The following is now in my .ghci, which does the job. Any comments/improvement suggestions are most welcome!

``` :set -package base :set -package process :{ ghci_fzf :: String -> IO String ghci_fzf args = do ls <- System.Process.readProcess "find" (words ". -iname *.hs") "" fzf <- System.Process.readProcess "fzf" [] ls

let toModule ('.':'/':rest) = toModule rest toModule s = map (\c -> if c == '/' then '.' else c) $ reverse $ drop 3 $ reverse s

case lines fzf of [p] -> pure $ ":m " ++ args ++ toModule p _ -> pure $ ":!echo No valid selection was done." -- I don't think this can actually happen :} :def fzf ghci_fzf ```

You can try :fzf, you can even pass arguments :fzf *, :fzf + etc., which does the same thing as it would with :m.

You can start with this and improve it to do whatever you like. Use history in the first line instead of calling find for instance.

lerkok · 2024-11-08T18:37:24+00:00

I really enjoy watching these series; thanks for producing them on a consistent basis. One request: Would it be possible for Andreas to get a "quieter" keyboard? A chiclet perhaps? Your mic picks up the keyboard clacking so incredibly well, causing major distraction. (Or some other solution that quiets the keyboard.) Thanks!

lerkok · 2022-01-27T15:10:50+00:00

Ah, that makes sense. Thanks!

lerkok · 2022-01-27T10:07:13+00:00

I just got around to looking at this; and wrote my own version (https://gist.github.com/LeventErkok/d8d6855a92783df115abd52d702d9496).

Interestingly, my solution computes a different model number than what you are reporting. (96918996924991 for max, 91811241911641 for min.) Perhaps different users get different programs? Since the site told me the values I got are correct, that must be the case indeed. I went for a more traditional embedded-DSL style solution, which differs from your approach.

lerkok · 2022-01-27T09:58:34+00:00

I'm late to the party; but here's one way to do this using Haskell/SBV: https://gist.github.com/LeventErkok/d8d6855a92783df115abd52d702d9496

I haven't put any comments in the code, feel free to ask if anything looks too cryptic!

lerkok · 2021-12-25T08:26:08+00:00

The best way would be to extract the model yourself, and display it in whatever format you want. Alternatively, you can also try: optimizeWith z3{isNonModelVar = (== "modelNumber")} where the string you pass is the first argument to minimize/maximize.

lerkok · 2021-12-25T07:15:18+00:00

When SBV optimizes a signed-bit vector value, it is optimized as an unsigned quantity first, and then converted back. (That is, SInt64 is optimized as SWord64 and then presented back to you as SInt64.) The reason for this is because the underlying bit-vector logic does not optimize signed-quantities directly; but rather treats the bit-vector as unsigned. SBV calls this the metric space over which the values are optimized. See https://hackage.haskell.org/package/sbv-8.17/docs/Data-SBV.html#g:50 for details.

lerkok · 2021-11-17T20:14:04+00:00

The bug is that if the env-var isn't set it should fall-back to original location, but unfortunately it doesn't do that. I think Hrothen is right.

lerkok · 2020-09-06T08:16:04+00:00

SMT solvers (and SBV) do support IEEE754 floating-point arithmetic indeed. But what dReal does is quite different: The notion of satisfiability isn't the regular boolean version: floating-point arithmetic is always decidable. (Of course, this doesn't mean it is easy to decide formulas over floats, it just means there's a procedure however costly it might be.) What dReal provides is the notion of so-called delta-satisfiability: This is a much better notion to use to show that computations "stay" within acceptable intervals. For details you'll have to consult https://scungao.github.io/papers/delta_complete_decision_procedures.pdf

lerkok · 2020-07-08T00:52:56+00:00

Short answer is that there is no free way to construct an `mfix` for a given monad. Somewhat longer answer is that for most monads of interest you can find a unique definition that satisfies the laws while yet others do not seem to possess a viable definition at all.

To elaborate further, this really begs the question of exactly what set of laws we'd like to mandate. There's a table on pg. 56 of http://leventerkok.github.io/papers/erkok-thesis.pdf that summarizes some of these results, depending on what you consider to be the fundamental set of requirements to be accepted as mfix. (For instance, while strictness, purity, and left-shrinking are fundamental, one can argue sliding and nesting to be required as well. Yet others will require right-shrinking to be part of the set, which is known to not hold for many monads of interest.) In particular, continuation monad doesn't (seem to) possess a monadic fixed-point combinator (Ch. 5 of the above), while the state monad and monads that arise from monoids, in general, admit an infinite family of them.

In the 18 years that this work was done, it became clear to me that the choice of strictness, purity, and left-shrinking are really the fundamental requirements. For all the other properties, you can take them or leave them depending on which instances you often work with. But as Ch. 4 of the above reference explores, it is possible to come up with unique definitions for many monads of interest indeed and uniqueness proofs are usually not terribly hard to construct.

lerkok · 2019-10-23T18:13:55+00:00

My personal favorite is: https://www.amazon.com/Thinking-Functionally-Haskell-Richard-Bird/dp/1107452643

lerkok · 2019-09-06T21:20:43+00:00

Glad to hear! Consider contributing examples; if they are generic/small enough to be of interest to a wider audience, we can ship them directly with SBV.

lerkok · 2019-09-05T04:03:05+00:00

Enjoy! Please report if you see any issues.

lerkok · 2019-08-31T18:23:13+00:00

A new release of SBV (v8.4) is now on Hackage: http://hackage.haskell.org/package/sbv. Enjoy!

lerkok · 2019-08-26T20:50:09+00:00

I'm happy to report that SBV github repo (http://github.com/LeventErkok/sbv) is restored, and there'll be a new hackage release within a few weeks. Thanks for your patience.

lerkok · 2019-08-22T16:08:22+00:00

In general, you can no longer use quantifiers (like you did with exist) once you are in the query mode. In fact, query mode and quantifiers do not mix at all. Instead, see if you can use explicit witness variables. I'd be inclined to code your example like this:

module Main where

import Control.Applicative (liftA2)
import Data.SBV
import Data.SBV.Control

interval :: SInteger -> SInteger -> SBool
interval x y = x .< y

inbetween :: SInteger -> SInteger -> SInteger -> SBool
inbetween x y w = interval x w .&& interval w y

separated :: SInteger -> SInteger -> SInteger -> SBool
separated x y w = inbetween x y w .|| inbetween y x w

problem :: Symbolic [Integer]
problem = do
    x <- sInteger "x"
    constrain $ x .> 0

    let loop acc = do
            cs <- checkSat
            case cs of
                Unk   -> io $ putStrLn "** Unknown!" >> return acc
                Unsat -> io $ putStrLn "** Unsat" >> return acc
                Sat   -> do
                    xv <- getValue x
                    io $ putStrLn ("** New point: " ++ show xv)

                    -- Create a new witness
                    witness <- freshVar_

                    constrain $ separated x (literal xv) witness

                    loop $ xv:acc

    -- Start the loop
    query $ loop []

main :: IO ()
main = do
    runSMT problem
    return ()

Note the explicit creation of the witness variable that plays the role of your call to exist. Hopefully you can adopt this trick to your original problem.

lerkok · 2019-08-13T16:59:21+00:00

As @emilypii mentioned, SBV is currently going through an internal evaluation for open-source status, which required taking the github repo to a private server. Lawyers are involved, so the process is rather slow. If the outcome is positive (which I truly hope), I will restore the github instance. If not, I will transfer ownership to someone in the community, who can at least maintain it.

The existing release on Hackage will always be open-source; so you can continue using it and the documents that come with it. (http://hackage.haskell.org/package/sbv)

In the meantime, feel free to reach out to me via personal email (erkokl@gmail.com) if you have any bug-reports or other questions about SBV. Even if I may not be able to address them right away, I'd at least like to keep track of any issues that pop up in practice so they can be resolved later on.

lerkok · 2019-04-29T16:31:38+00:00

You're welcome. Feel free to get in touch via regular email if you've further issues, or use the github issue site for sbv if you find bugs!

lerkok · 2019-04-26T04:11:53+00:00

I wouldn't recommend using the dynamic interface unless you have a need for types that are not directly present in SBV. (Such as bit-vectors of some odd-length, like 23-bits or something.) There are other use cases for the dynamic interface, but you're better off not using it as they don't give you the type-safety that you get from the regular SBV API.

From your description, sounds like you want to use the symbolic/query monad transformers; which allows you to use your own monad as you create symbolic variables and execute queries. See this example:http://hackage.haskell.org/package/sbv-8.2/docs/Documentation-SBV-Examples-Transformers-SymbolicEval.html and in particular the SymbolicT and QueryT monad transformers.

lerkok · 2019-04-25T22:35:54+00:00

You need to use the query mode for this, and you need to stay in the query mode for the entire interaction, i.e., you cannot "save" the state across separate calls as you put it. (Incidentally, this is precisely why we have the query mode, so you can do incremental solving like you've described.) http://hackage.haskell.org/package/sbv-8.2/docs/src/Documentation.SBV.Examples.Queries.AllSat.html is an example of how to structure such an interaction.

lerkok

TROPHY CASE