Where communities thrive

  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
  • Oct 21 2017 21:21
    @jpitts banned @Musk55
<d-xo> which seems to suggest that >>Int is translated to shrInt in smt, but I can't find a definition of shrInt anywhere?
<ehildenb> @d-xo sorry for the much delayed response!
<ehildenb> For the most part, we try do deal with any bitwise operations via algebraic reasoning (rewrites over expressions), rather than some bit-blasting approach or something.
<ehildenb> And I think it's the correct way to do it.
<ehildenb> Bit-blasting I think makes very little sense for software verification honestly. Most software is not doing bit-level manipulations.
<ehildenb> And EVM bytecode that comes from the Solidity compiler (and likely other compilers) have very regular structure.
<ehildenb> So bit-level operations on words are to project out chunks of bits for packed storage slots for the most part.
<ehildenb> Which can be represented algebraically much cleaner.
<ehildenb> For example, something like maxUInt48 &Int (X >>Int 48) means "give me the second lowest 48 bits"
<ehildenb> And if that's what you want, then you can just have a rule like rule maxUInt48 &Int (X >>Int 48) => projectSecondLowest48(X)
<ehildenb> Then axiomatize projectSecondLowest48 directly.
<ehildenb> Or you can have more generic project... functions which can be used.
<ehildenb> But the point is to take advantage of the structure that the compiler introduces. It's not like it will introduce arbitrary bitwise operation, but highly structured ones. bit-blasting gives up completing on understanding that structure.
<ehildenb> Here, for example, is the algerbraic presentation of the needed packing/unpacking lemmas for multi-collateral dai: https://github.com/runtimeverification/evm-semantics/blob/master/tests/specs/mcd/word-pack.k
<ehildenb> So the short answer is "we don't deal with things like shifts directly, we try to handle it at a higher-level, in a Solidity-specific or even contract-specific way"

<anvacaru> @leonardoalt I've changed the Dockerfile-eldarica to use your suggested soljson file. When an assertion violation happens I get a large output which starts with

  auxiliaryInputRequested: {
    smtlib2queries: {
      '0x5e7df8f9c2da419124ac9c1918697f4d25bea8f5918512e44855c3ee108eb46f': '(set-logic HORN)\n' +
        '\n' +
        '(declare-datatypes ((|state_type| 0)) (((|state_type| (|balances| (Array Int Int))))))\n' +


I did not get any counter examples. Instead, I get a message at the end saying that there were no Horn solvers available.

      component: 'general',
      errorCode: '3996',
      formattedMessage: 'Warning: CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.\n' +
      message: 'CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.',
      severity: 'warning',
      type: 'Warning'
<leonardoalt> @anvacaru in that case it looks like it's not finding the solver at all
<leonardoalt> which is very weird if the script didn't change
<anvacaru> I only ran make build in order to build the tool. Was I supposed to do any additional steps to install the solver?
Wait, make build for which tool?
<anvacaru> make build for the SMT Checker, which would build the docker images.
<leonardoalt> hmm not sure I get it. The soljson.js file is already the compiler binary with smtchecker
<leonardoalt> so the only thing you need to do is change the .ts script to enable -cex and -ssol for Eldarica, and copy the new soljson I sent into the docker image instead of the old one

<Sam Richards (samajammin)> Hey folks! Curious what people think about this & if anyone would be interested in helping 🙂



<Kademlia> For anyone interested, this morning I've cut the very first open sourced release of Athena (for those who are unfamiliar, Athena is a natural-deduction based language and proof development framework).

In the coming months, Athena will be used for:

  1. Constructing abstract models of some key DeFi protocols
  2. Verifying specifications about EVM code
  3. An open sourced curriculum for learning formal verification to a professional level

<Sam Richards (samajammin)> Hey folks - a community member has submitted a PR 🤩 !

Appreciate if anyone could review this for correctness & overall quality: ethereum/ethereum-org-website#6394

Please & thanks 🙏