[HN Gopher] Haroldbot, client-side tool that checks 32-bit bitve...
       ___________________________________________________________________
        
       Haroldbot, client-side tool that checks 32-bit bitvector arithmetic
       equivalence
        
       Author : lifthrasiir
       Score  : 36 points
       Date   : 2023-11-15 09:04 UTC (13 hours ago)
        
 (HTM) web link (haroldbot.nl)
 (TXT) w3m dump (haroldbot.nl)
        
       | someplaceguy wrote:
       | This is very cool, especially the automatic proof generation!
       | 
       | That said, I wonder if it would make more sense to use an SMT
       | prover as fallback rather than a SAT solver. The latter requires
       | converting the 32-bit operations into boolean circuits, which
       | might not be the most efficient way to solve the problem
       | considering modern SMT solvers such as Z3 and CVC5 already have
       | built-in efficient support for bit-vectors?
       | 
       | In fact, I believe that's what Alive2 [1] does, which is a
       | similar tool (although with slightly different goals).
       | 
       | I think it might even be possible to make this work for 64-bit
       | vectors with SMT (in most cases).
       | 
       | [1] https://github.com/AliveToolkit/alive2
        
         | IshKebab wrote:
         | Yeah I'm pretty sure Z3 can do all the examples easily. Nice
         | simple interface though!
        
           | Randor wrote:
           | Yep, Z3 can do exactly this using BitVec and passed to
           | prove() or just compare the expressions directly..
        
       | cole-k wrote:
       | The way they do search reminds me a lot of
       | https://herbie.uwplse.org/
        
       | lobf wrote:
       | I work in the film industry, not tech, but I like to read hacker
       | news and see what's new with you programmers.
       | 
       | Just in case nobody else is far enough outside the industry to
       | tell, this is a hilariously nonsensical post title for us
       | ignorant laymen. It sounds like a fake product out of HBO's
       | Silicon Valley.
        
       ___________________________________________________________________
       (page generated 2023-11-15 23:00 UTC)