Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
  • Oct 21 2017 21:21
    @jpitts banned @Musk55
Eth-Gitter-Bridge
@Eth-Gitter-Bridge
<ehildenb> Either way I'll make my way to Amsterdam, and I'm sure we'll all run into each other!
<ehildenb> Also, if anyone here is going to Eth Denver, I live 1.5 hours from there, would be down to meet up!
Eth-Gitter-Bridge
@Eth-Gitter-Bridge
<leonardoalt> @ehildenb yep, that's all! devconnect won't have a central registration, every event has their own.
Nice! Looking forward to meeting everyone
Eth-Gitter-Bridge
@Eth-Gitter-Bridge
<ehildenb> @leonardoalt can you provide instructions for @anvacaru to build your experimental version?
Eth-Gitter-Bridge
@Eth-Gitter-Bridge
<leonardoalt> @ehildenb @anvacaru I need to rebase the main branch on that one and it's getting late, will send tomorrow 🙂
Eth-Gitter-Bridge
@Eth-Gitter-Bridge
<leonardoalt> @ehildenb @anvacaru sorry for the delay, but here it is:
https://output.circle-artifacts.com/output/job/f0d73a61-d44a-4070-84a1-d1229293600f/artifacts/0/soljson.js
you can try to run Eldarica with this soljson, it has some support to counterexamples and invariants from Eldarica.
Please let me know if it works!
Eth-Gitter-Bridge
@Eth-Gitter-Bridge
<Kademlia> putting together a collection of examples of programming proofs, proof procedures, etc. Dropping here in case it is interesting to anyone https://github.com/WilfredTA/proof-programming
Eth-Gitter-Bridge
@Eth-Gitter-Bridge
<ehildenb> Thank you! We will take a look and let you know 🙂
Eth-Gitter-Bridge
@Eth-Gitter-Bridge
<d-xo> @ehildenb how does k deal with bitshifting ints at the smt level? Do you use int_to_bv and bv_to_int?
<d-xo> which seems to suggest that >>Int is translated to shrInt in smt, but I can't find a definition of shrInt anywhere?
Eth-Gitter-Bridge
@Eth-Gitter-Bridge
<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
Eth-Gitter-Bridge
@Eth-Gitter-Bridge
<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"
Eth-Gitter-Bridge
@Eth-Gitter-Bridge

<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' +
        '\n',
      message: 'CHC analysis was not possible. No Horn solver was available. None of the installed solvers was enabled.',
      severity: 'warning',
      type: 'Warning'
    }
  ],
Eth-Gitter-Bridge
@Eth-Gitter-Bridge
<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
Eth-Gitter-Bridge
@Eth-Gitter-Bridge
<anvacaru> I only ran make build in order to build the tool. Was I supposed to do any additional steps to install the solver?
leo
@leonardoalt:matrix.org
[m]
Wait, make build for which tool?
Eth-Gitter-Bridge
@Eth-Gitter-Bridge
<anvacaru> make build for the SMT Checker, which would build the docker images.
Eth-Gitter-Bridge
@Eth-Gitter-Bridge
<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
Eth-Gitter-Bridge
@Eth-Gitter-Bridge
Eth-Gitter-Bridge
@Eth-Gitter-Bridge

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

ethereum/ethereum-org-website#6194

Eth-Gitter-Bridge
@Eth-Gitter-Bridge

<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
xvwx
@xvwx:matrix.dapp.org.uk
[m]
congrats!
Eth-Gitter-Bridge
@Eth-Gitter-Bridge

<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 🙏