itamarst has quit [Quit: Connection closed for inactivity]
[Arfrever] has quit [Ping timeout: 240 seconds]
[Arfrever] has joined #pypy
<arigo_>
cfbolz: that's very random, but thinking again about a JIT that stores and reuses already-compiled loops
<arigo_>
in theory, it can be done by recording all operations and guards in the metainterp *including the ones on constants*
<cfbolz>
arigo_: right, interesting
<cfbolz>
But we would have to trace to reuse, right? Just not use the backend?
<arigo_>
the idea would be to allow a very fast tracing, at least if we assume there is just one existing loop and we just want to check if the running code would generate the same loop
<arigo_>
unsure if that would work in practice or be completely defeated by the fact that the next time you fast-trace, you're likely to see a different branch first
<cfbolz>
ah, it's a tracing that can be a bit like the black hole in that it doesn't actually trace
<cfbolz>
just check constants?
<arigo_>
something like that
<arigo_>
so check that the constant guards give the same result, and also record the constant arguments that go into residual operations
<cfbolz>
for "linking", basically
<arigo_>
yes
<cfbolz>
I still think I would want to write a prolog version first to understand this 😅
<arigo_>
yes :-)
<cfbolz>
arigo_: quite a different topic, but I'm having quite some fun with Z3 (the smt solver) again recently
<arigo_>
OK?
<cfbolz>
I realized that it's variable objects have all operators overloaded, which means you can pass them into helper functions that do bit manipulations
<cfbolz>
*its
<cfbolz>
As long as the helpers have no control flow
<cfbolz>
Then you get a big formula term back
<cfbolz>
And then you can ask Z3 to find counterexamples for properties that you would like to be true
<arigo_>
OK
<cfbolz>
It's a bit like hypothesis, except that if Z3 says that no counterexamples exist, you really have a proof
<arigo_>
cool
<cfbolz>
I'm using it to verify the logic in the 'known bits' branch, which I'm somewhat worried about
<cfbolz>
which is why it's not merged since two years :-)
<cfbolz>
nimaje: yes, sure. I can also compare against cvc5, but at some point you have to stop
<cfbolz>
arigo_: what I like a lot is the fact that you can really 'run' the code, so you don't have the problem of formal verification where the code that you prove something about is not at all the code that runs
<nimaje>
yeah, it is unlikely that you run into some soundness bug, but you should remember that they can exist, does the logic you use have some proof certificate output and some proof verifier? it is even less likely that a verifier has a soundness bug, as it is smaller and if it is developed independently, the intersection of bugs is likely small
<cfbolz>
👍
<cfbolz>
(I'm actually part of a formal methods research group, usually our interaction is a bit limited though)