What does HackerNews think of z3?

[0]https://github.com/Z3Prover/z3

[1]https://nim-lang.github.io/Nim/drnim.html

Yes, rather than demand others cater to your whims, frankly.

Do you realise how hypocritical it sounds to complain that you are not proficient in Javascript, when others might not be proficient in ?

Go use Z3 if you need a prover in C++ (or Java), its far more robust (provided its the type you're after) than someones 700 LoC JavaScript implementation.

https://github.com/Z3Prover/z3

  // Code to demonstrate finding the hidden seed of a PRNG with Z3
  // Chris Lomont Oct 2021
  // Answering this comment on Hacker News https://news.ycombinator.com/item?id=28886698

  // Start by getting Z3, a theorem prover from Microsoft, via nuget. See https://github.com/Z3Prover/z3
  using Microsoft.Z3;
  using System;

  // get a solution
  ulong Solution(Context ctx, BoolExpr f, BitVecExpr seed)
  {
    Solver s = ctx.MkSolver();
    s.Assert(f); // assert constraint into solver
    if (s.Check() == Status.SATISFIABLE)
    {
        var m = s.Model;
        Expr e = m.Evaluate(seed);
        return ulong.Parse(e.ToString());
    }
    else
        throw new Exception("Fatal error");

  }

  // simple PRNG, used in many old C libs
  UInt32 next = 0x1234;
  UInt32 rand()
  {
    next = next \* 214013 + 2531011;
    return (next / 65536) % 32768;
  }

  void Test()
  {
    var R = new Random();
    next = (uint)R.Next();
    var start = next;
    Console.WriteLine($"Starting seed {next:X8}");

    using (var ctx = new Context())
    {
        // 32 bit vector type
        Sort bv_type = ctx.MkBitVecSort(32);

        // unknown seed - we will solve for this
        BitVecExpr seed = ctx.MkBVConst("seed", 32);

        // constants used in the PRNG
        BitVecExpr c214 = (BitVecNum)ctx.MkNumeral("214013", bv_type);
        BitVecExpr c253 = (BitVecNum)ctx.MkNumeral("2531011", bv_type);
        BitVecExpr c65536 = (BitVecNum)ctx.MkNumeral("65536", bv_type);
        BitVecExpr c32768 = (BitVecNum)ctx.MkNumeral("32768", bv_type);

        // track the boolean to satisfy
        BoolExpr be = ctx.MkTrue();

        var next = seed; // start here
        int pass = 0;
        while(true)
        {
            ++pass;
            if (pass > 10) break;
            // the sampled random
            var r = rand();
            BitVecExpr rndBV = (BitVecNum)ctx.MkNumeral(r, bv_type);

            // make this code using Z3 variables
            //next = next * 214013 + 2531011;
            //return (next / 65536) % 32768;
            next = ctx.MkBVAdd(ctx.MkBVMul(next, c214), c253);
            var ret = ctx.MkBVURem(ctx.MkBVUDiv(next, c65536), c32768);

            // add a constraint boolean for this "Z3 ret = returned value"
            be = ctx.MkAnd(be, ctx.MkEq(ret, rndBV));

            // get solution
            var val = Solution(ctx, be, seed);
            // todo - can check unique by adding "seed != soln" to the boolean and checking
            Console.WriteLine($"{pass} : 0x{val:X8}");
            if (val == start)
                break; // done - can also break when shown unique
        }
    }
  }
  Test();

a) "use Z3[0] with some binary/source-language-of-choice/LLVM -lifting to handle relatively simple situations that need to": i) guarantee some assert (often, but not always index-out-of-bounds checks, like non-trivial Rust slice indexing) statements are unreachable ii) some bit hacks compute the same thing as the non-hacked implementation

b) "use TLA+[1] to verify concurrent stuff with race conditions": i) in lock-free data structures that don't come with a proof that the algorithms do the right thing (in those cases, just verify three implementation truly matches the proven algorithm) ii) in (network, or sufficiently network-like) protocols that aren't 100% exactly transcribed ports of existing proven algorithms or so simple a finite state machine can (and will) be used

2) For doing it more for fun than short-term gains: a) For getting a handle on pure functional program design, I recommend going through the relevant track of HtdP[2] (Prologue until just before "Arithmetic and Arithmetic" -> I -> II -> III -> Intermezzo 2: Quote, Unquote -> V {-> [if you want to write remotely-performant pure functional code, follow up with:] VI}) b) For learning how to exploit a proof assistant for fun and applied computer science, I'll refer to the guidance provided by Isabelle/HOL. Please use the IRC(/Matrix ?)[3] if you are confused on how exactly to best approach Isabelle/HOL in your case.

[0]: https://github.com/Z3Prover/z3 [1]: https://lamport.azurewebsites.net/tla/tla.html [2]: https://htdp.org/2021-5-4/Book/index.html [3]: [edit: apparently it is neither IRC nor Matrix, but rather Zulip:] https://isabelle.zulipchat.com/

https://github.com/Z3Prover/z3

It has bindings for other languages and is able to make some rather sophisticated arithmetical and logical deductions in an often pretty efficient way. I've used it successfully for parts of puzzle competitions and CTFs (and I'm really only beginning to scratch the surface of what it can do).

You can read more about the options in that area at

https://en.wikipedia.org/wiki/Satisfiability_modulo_theories

which also links to the related tools in

https://en.wikipedia.org/wiki/Answer_set_programming

https://en.wikipedia.org/wiki/Constraint_programming

These systems can feel pretty magical and are getting more powerful all the time. (Of course there are cases where there is a better algorithm that you could find, perhaps a much more efficient one, and using these solvers will be asymptotically or worst-case slower than it had to be given more human insight.)

Some of these could be overkill for your application, and Z3 doesn't have a Javascript binding, so I guess it's not as helpful for web forms.

https://github.com/Z3Prover/z3

  (declare-const a1 Bool)
  (declare-const a2 Bool)
  (declare-const a3 Bool)
  (declare-const a4 Bool)
  (declare-const a5 Bool)
  (declare-const a6 Bool)

  (assert (= a1 (and a2 (and a3 (and a4 (and a5 a6))))))
  (assert (= a2 (not (or a3 (or a4 (or a5 a6))))))
  (assert (= a3 (and a1 a2)))
  (assert (= a4 (or a1 (or a2 a3))))
  (assert (= a5 (not (or a1 (or a2 (or a3 a4))))))
  (assert (= a6 (not (or a1 (or a2 (or a3 (or a4 a5)))))))
  (assert (or a1 (or a2 (or a3 (or a4 (or a5 a6))))))

  (check-sat)
  (get-model)
  (exit)

Additionally forcing a5 to be false by adding the following to the list of assertions:

  (assert (not a5))

Edit: Finally, to make sure there's not some possible solution where a5 is true as well as another assertion you could alternatively add this assertion:

  (assert (and a5 (or a1 (or a2 (or a3 (or a4 (or a6)))))))

[0] https://github.com/Z3Prover/z3

[1] https://rise4fun.com/Z3/1DMW

The search space for this problem is enormous, but Z3 will produce an impressive result within a few minutes.

https://github.com/Z3Prover/z3

Is it comparable with prolog or just a subset of prolog?

To be able to state that a piece of software is bug-free and formally correct, we first need a notion of correctness: that the algorithm follows a [formal] specification.

The first step would be to formally specify what the software/algorithm should do. Then, the next step would be to use formal methods and mathematical tools (e.g. set theory and logic) to prove that your algorithm does exactly as the specification says.

TLA+ is a formal method that can be used for writing specifications and model-checking them. While a big step forward from testing, model-checking still doesn't "prove" anything.

For proving, you can use theorem provers like the Z3 [0] SMT solver (or a formal framework that uses theorem provers) to do proof checking.

The Event-B [1] method is one such formal method that uses SMT solvers and allows you to model systems starting with a very abstract and high-level model, state invariants about your system, and prove that those invariants hold as you refine your models and make them more concrete.

Feel free to shoot me an email if you like to talk more about formal methods :)

[0]: https://github.com/Z3Prover/z3

[1]: http://www.event-b.org/

Z3 (https://github.com/Z3Prover/z3) is the Satisfiability Modulo Theories (SMT) solver to use. It is such a quality piece of software and it's amazingly easy to find help on StackOverflow from the main developers. Z3 really is the default choice for an SMT solver these days (i.e. you only reach for other solvers when you really have to).

Roslyn (https://github.com/dotnet/roslyn) is the C# (and VB) compiler as a library. Useful for doing code analysis and code generation for a modern imperative language. Roslyn is a whole lot easier to get started with than integrating Clang/LLVM into a project, so it really lowers the barrier of entry for lightweight program analysis projects.