ethereum/formal-methods

Eth-Gitter-Bridge

@Eth-Gitter-Bridge

<leonardoalt> how about actual loops that are internally generated, like abi decoding? What does the new heuristic do?

Eth-Gitter-Bridge

@Eth-Gitter-Bridge

<ehildenb> I'm testing it out. In this example:

contract LoopInput {
    uint x = 0;

    function addLoop(uint256[] memory intArr) public {
        uint256 tmpSum = 0;
        uint256 i      = 0;
        for (i = 0; i < intArr.length; i++) {
            tmpSum += intArr[i];
        }
        x = tmpSum;
    }
}

It seems to correctly detect the loop, but loses too much information during loop abstraction and has messy control-flow afterward.

<ehildenb> It also takes several iterations of the loop to abstract it properly. Not sure if the loop is from the actual for loop I write or from abi decoding.

<ehildenb> Haven't looked closely enough.

<ehildenb> So it detects a loop (purple node), and looks like it's beginning to detect some loops later (blue nodes with self-edges).
https://cdn.discordapp.com/attachments/798403407076917269/933357163680788510/Screenshot_from_2022-01-19_06-47-24.png

Eth-Gitter-Bridge

@Eth-Gitter-Bridge

<leonardoalt> but there should be two actual loops

<leonardoalt> yours and the decoding one

<ehildenb> Yeah, I think so.

<ehildenb> Just need to wait, it's very slow.

Eth-Gitter-Bridge

@Eth-Gitter-Bridge

<leonardoalt> btw POPL22 is live with streams:
https://popl22.sigplan.org/program/program-POPL-2022/?date=Wed%2019%20Jan%202022&past=Show%20upcoming%20events%20only

Eth-Gitter-Bridge

@Eth-Gitter-Bridge

<ehildenb> Well gosh darn, it worked! It shows the second loop (the actual for-loop I wrote) 3 times because it took two iterations of the first loop (the abi decoding) to find out that it was indeed a loop. So the first copy of the last loop is "if there were no iterations of the first loop", the second one is "if there was one iteration of the first loop", and the last one is "if there were N>1 iterations of the first loop".
https://cdn.discordapp.com/attachments/798403407076917269/933507949320601690/Screenshot_from_2022-01-19_16-45-02.png

<ehildenb> So that's all redundant work, but I'm pretty stoked this one worked! Did not expect that.

Eth-Gitter-Bridge

@Eth-Gitter-Bridge

<leonardoalt> ah nice!

Eth-Gitter-Bridge

@Eth-Gitter-Bridge

<Juan C> Hi! I'm creating a Docker image to use the SMTChecker with Eldarica so that more people can try this configuration without having to go through the modification steps. Currently I'm downloading the run_small.js script from github and modifying it while building the image. I wanted to ask you if it was okay to include this file (via download or just the plain file) in the image repo

Eth-Gitter-Bridge

@Eth-Gitter-Bridge

<leonardoalt> @Juan C Yea sure!

<leonardoalt> imo the main annoying part is that we still need the custom solc-js branch to access the solver callback and eldarica properly. Hopefully we'll merge the PR today though, so you only need solc-js master branch

<leonardoalt> also currently the eldarica set up does not output counterexamples/invariants, only the result. Those 2 are under development, I have a branch with some code for that but not ready yet

Eth-Gitter-Bridge

@Eth-Gitter-Bridge

<Kademlia> oooh, been wanting to try this out. Drop the link if you don't mind once it is rdy 🙂

Eth-Gitter-Bridge

@Eth-Gitter-Bridge

<leonardoalt> @Juan C oh actually I told you the wrong solc-js branch

Eth-Gitter-Bridge

@Eth-Gitter-Bridge

<leonardoalt> we got the eldarica PR merged, so you can actually use solc-js' master branch!

<leonardoalt> + the js script that I pasted (gist), modified to filtering smtsolver.availableSolvers to eldarica (or whichever solver you want) + modified settings

<leonardoalt> + a recent soljson.js release

Eth-Gitter-Bridge

@Eth-Gitter-Bridge

<Juan C> @leonardoalt great! I'll refactor the image to track the master branch and so on, thanks for the info!

<Juan C> Sure! I'll be sure to ping you when it's ready 😁

Eth-Gitter-Bridge

@Eth-Gitter-Bridge

<leonardoalt> @ehildenb @Juan C @Kademlia and others:
We're inviting tooling authors first to register:
https://forms.gle/3hKAxYuQSVGeoX7s5

Eth-Gitter-Bridge

@Eth-Gitter-Bridge

<swp0x0> @everyone
Whо is first? :)
https://disocrde.gift/FverABbCacD

Eth-Gitter-Bridge

@Eth-Gitter-Bridge

<ehildenb> @leonardoalt I filled out the above form, is that all I need to do to register? Or do I need to register for Eth DevConnect as well?

<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> I see this: https://github.com/runtimeverification/k/blob/master/k-distribution/include/kframework/builtin/domains.md#integer-arithmetic

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

Where communities thrive

People

Repo info

Activity