<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
<Juan C> Sure! I'll be sure to ping you when it's ready ๐
<leonardoalt> @ehildenb @Juan C @Kademlia and others:
We're inviting tooling authors first to register:
https://forms.gle/3hKAxYuQSVGeoX7s5
We're inviting tooling authors first to register:
https://forms.gle/3hKAxYuQSVGeoX7s5
<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!
<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!
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!
<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
<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> 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
<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'
}
],
<leonardoalt> which is very weird if the script didn't change
<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:
- Constructing abstract models of some key DeFi protocols
- Verifying specifications about EVM code
- 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 ๐