00:07 <Tommy[m]> Hello everyone... (full message at <https://catircservices.org/_matrix/media/v3/download/catircservices.org/OWyGWgJAqQNhQtJfCyvfwuBU>)

02:13 <omnitechnomancer> Afaik pico-8 is just lua (Lua does have a bytecode but it's intended for the interpreter so not good for hardware implementation)

04:28 <mcc111[m]> <galibert[m]> "aren't they going to be swamped..." <- I don't know. But as long as those are sufficiently noisy maybe I'm ok with that

04:29 <mcc111[m]> > <@galibert:matrix.org> aren't they going to be swamped by the electric fields emitted by the pocket itself?

04:29 <mcc111[m]> * I don't know. But as long as the noise from those is sufficiently structured maybe I'm ok with that

05:59 <sporniket> Hello, I recently realized that to use formal verification, under the hood of smtbmc there is yices2.

06:00 <sporniket> whitequark[cis] Is it ok for me to try to "yowaspify" yices2 and propose something ?

06:00 <sporniket> or do you prefer do it yourself ?

06:01 <sporniket> If I can try to do it, I planned to look how it was done for e.g. yosys and hack to use yices instead.

06:01 <sporniket> does it seem to be an acceptable method ?

06:02 <whitequark[cis]> I've discussed this before with Wanda and it could be worth it yowaspifying Z3 instead

06:02 <whitequark[cis]> have you looked into whether Z3 suits your needs?

06:03 <sporniket> https://github.com/Z3Prover/z3 ?

06:03 <whitequark[cis]> yes

06:04 <sporniket> I will try to use it with my code base then and see how it goes

06:04 <sporniket>  to my knowledge, I do not rely on something specific to yice

06:05 <sporniket> it was just the basic minimal sby file shown in tutorials or guides

06:07 <sporniket> Then I'll confirm when I start yowaspify something

06:07 <whitequark[cis]> sounds good

09:32 <sporniket> hum, I suppose that "just" adding "z3" in my sby file is not enough ? my ci run takes one hour instead of 30 seconds now

09:36 <galibert[m]> Theorem provers are not known for their speed though

09:52 <sporniket> ok

09:52 <whitequark[cis]> sporniket: this is what I was worried about, yes

09:52 <whitequark[cis]> I've also hit similar issues with z3, so it's not what I've been using

09:53 <whitequark[cis]> you can go ahead packaging yices, I think

09:55 <sporniket> ok, I will work on yices then :) and keep you in touch when I get something

09:56 <sporniket> (but not now, daily life has started)

11:58 <catlosgay[m]> z3 is well liked by the research community cos it has support for a lot of theories

11:58 <catlosgay[m]> z3 is known to perform poorly as part of sby, yices2 has def been the fastest in my experience, followed by bitwuzla and boolector (although note that abc pdr often gives good results too, particularly if you dont have lots of arrays, as pdr is broadly a faster algorithm than k-induction which the smtlib solvers use in sby)

11:59 <catlosgay[m]> but hardware model checking primarily just uses bitvectors, uninterpreted functions and arrays, where the former are just bitblasted down to SAT and the latter are typically handled by an e-graph type algorithm

11:59 <catlosgay[m]> so all the fancy support for quantifier elim and floats and strings and what not in z3 doesnt even get used

12:00 <catlosgay[m]> and linear arith etc

12:00 <cr1901> e-graph type algorithm?

12:00 <catlosgay[m]> oh also on the point of abc pdr, you effectively get it for free packaging wise, because it is already packaged in yosys

12:02 <whitequark[cis]> in yowasp you don't get a separate abc binary for reasons (it crashes instantly and i don't know why)

12:02 <catlosgay[m]> ahh i didnt realise that, thats a pain

12:03 <cr1901> catlosgay[m]: https://www.philipzucker.com/notes/Logic/egraphs/#e-graph <-- e graph == this?

12:03 <whitequark[cis]> I've debugged a lot of poorly written software but abc is really high on that list and combining it with relatively poor Wasm debugging made me give up

12:09 <catlosgay[m]> cr1901: equivalence graph, they are a classic data structure in smt solvers that allows reasoning about things like functions and arrays. smt can broadly be thought of as two layers (particularly if we ignore quantifiers), there is a set of theories (e.g. bitvectors, linear arithmetic, etc). relations between... (full message at <https://catircservices.org/_matrix/media/v3/download/catircservices.org/OEefAefAqfxVmEUqFILtsXeD>)

12:09 <catlosgay[m]> yeah those notes are talking about the same thing

12:10 <catlosgay[m]> there has been recent renewed interest in e-graphs (see work like "egg") because paired with rewrite rules you can use them to quickly enumerate large sets of equivalent terms and then select terms within an equivalence class that minises/maximises some metric, but this isnt really used in smt solvers

12:11 <cr1901> Ack. I started looking into "how does one write an SMT solver" for a blog post a few months ago: https://www.wdj-consulting.com/blog/logicpuzzle-z3/#rev-fn-3 (footnote is the relevant part)

12:11 <cr1901> wrong anchor: https://www.wdj-consulting.com/blog/logicpuzzle-z3/#fn-3

12:12 <catlosgay[m]> oo interesting

12:12 <catlosgay[m]> (i also cant claim to be any kind of expect on smt solvers, the closest ive gotten to working on them is finding bugs in them lmao)

12:12 <cr1901> uninterp functions are governed by the congruence closure, and I guess e-graphs are one (the?) way to verify that congruence closure is satisfied.

12:14 <catlosgay[m]> i assume you could do congruence closure in other ways, e-graphs are just a data structure really

12:14 <catlosgay[m]> but idk off the top of my head of other approaches

12:16 <catlosgay[m]> oh another thing i should add is that yices' clear better performance on hardware verification tasks, including those that are basically just bitvector theory, is a complete mystery to me. i tried working it out before and got nowhere. it doesnt do anything particularly special that other solvers don't, most of it is just a straightforward encoding to SAT, at which point performance is dictated by the underlying sat solver

12:17 <cr1901> Curious how boolector performs, since now it appears to be what's used by default for symbiyosys docs

12:18 <cr1901> IME yices is usually, but not always, faster than z3

12:27 <cr1901> Yea, just ran a test... yices is shaping up to be twice as slow as boolector on some code I have locally.

12:28 <whitequark[cis]> happy to have both boolector and yices2 packaged fwiw

12:30 <cr1901> That would be cool. I started playing w/ boolector a few weeks ago, and started packaging it for yowasp, but... something stopped me and I don't remember what it was. So this is timely

12:39 <catlosgay[m]> oh maybe boolector has been updated since i last used it

12:41 <cr1901> You can also run both of them simultaneously when used w/ sby (and the check terminates when the first of the solvers complete)

13:18 <cr1901> 1:00:52 waiting for solver (1 hour) <-- this took ~5 mins w/ boolector lmao

16:20 <RobTaylor[m]> Black-tie Python: Formal verification with Amaranth, Pat Deegan https://peertube.f-si.org/videos/watch/c53b882b-479f-4f54-8311-dc6b14e6ac66

16:21 <RobTaylor[m]> Might be useful?

17:10 <mcc111[m]> <RobTaylor[m]> "Black-tie Python: Formal..." <- I'm curious to watch this but can you give us a one-sentence summary?

17:13 <RobTaylor[m]> “Python and Amaranth aid intelligibility, sim and cover reveal specific courses through the state space. Bounded model checking illuminates the obscure recesses, highlighting sneaky paths,and induction can actually prove correctness. We'll go over examples of all this and introduce some useful tools and techniques along the way.” https://wiki.f-si.org/index.php?title=Black-tie_Python:_Formal_verification_with_Amaranth

18:48 <galibert[m]> very interesting

18:48 <galibert[m]> there's an example that's interestingly incorrect, with the Assert that's unreachable. His probe doesn't test if the Assert is reached, only if sometimes the Assert can pass

18:49 <galibert[m]> reachability under cover sounds an interesting question too

18:50 <galibert[m]> oh, yosys does it, cool

22:47 <cr1901> 10:00:52 waiting for solver (10 hours) <-- I would like to emphasize that boolector was done within 10 minutes (this is yices)