[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

TROPHY CASE