SMTChecker

[0x4007]

We should do the initial setup of this https://docs.soliditylang.org/en/v0.8.19/smtchecker.html

I presume there will be modifications we need to do to the code to get this to work, those can be in separate bounties after this is feature is set up.

https://twitter.com/paulrberg/status/1627654614811115520?s=46&t=lQUXMD9A0xd14FiMGl8IEQ

[d-roak]

Hi @pavlovcik

Can you assign this bounty to me?

[ubiquibot[bot]]

@jpldcarvalho The time limit for this bounty is on 3/9/2023

[ubiquibot[bot]]

Do you have any updates? @jpldcarvalho

[d-roak]

Have been busy last couple of days. I plan picking this again over the next week, feel free to reassign it to another person if needed 🙂

[0x4007]

The bot should automatically unassign you if you do not reply after a full week of inactivity!

[ubiquibot[bot]]

Do you have any updates? @jpldcarvalho

[ubiquibot[bot]]

Releasing the bounty back to dev pool because the allocated duration already ended!

[0x4007]

@0xcodercrane until we officially transition to making "no assignee" the default DevPool role, the bot should technically reassign to @ubiquity-bounties!

[chrlschwb]

/start

[0x4007]

/start

[ubiquibot[bot]]

Skipping /start since the issue is closed

[ubiquibot[bot]]

@chrlschwb The time limit for this bounty is on 4/4/2023

[0x4007]

@chrlschwb sorry we were doing maintenance on the bot this week and you must have attempted the assign command just as it went down! Please feel free to work on this!

[ubiquibot[bot]]

Do you have any updates @chrlschwb? If you would like to release the bounty back to the DevPool, please comment /unassign

[ubiquibot[bot]]

Releasing the bounty back to dev pool because the allocated duration already ended!

[FibrinLab]

@pavlovcik is this still an active issue. It's quite confusing with the comments.

[0x4007]

@pavlovcik is this still an active issue. It's quite confusing with the comments.

Yes it's available. You can tell from the lack of assignee on the issue!

[FibrinLab]

/start

[ubiquibot[bot]]

Skipping /start since the issue is closed

[ubiquibot[bot]]

Do you have any updates @FibrinLab? If you would like to release the bounty back to the DevPool, please comment /unassign

[FibrinLab]

Do you have any updates @FibrinLab? If you would like to release the bounty back to the DevPool, please comment /unassign

Waiting for review

[0x4007]

You should re-request reviews from specific reviewers once you incorporated their feedback.

[ubiquibot[bot]]

Do you have any updates @FibrinLab? If you would like to release the bounty back to the DevPool, please comment /unassign

[FibrinLab]

Do you have any updates @FibrinLab? If you would like to release the bounty back to the DevPool, please comment /unassign

I have updates

[0x4007]

You should re-request reviews on the pull request when you implement changes from our reviews.

[ubiquibot[bot]]

Do you have any updates @FibrinLab? If you would like to release the bounty back to the DevPool, please comment /unassign

[ubiquibot[bot]]

Releasing the bounty back to dev pool because the allocated duration already ended!

[0x4007]

@0xcodercrane check this assign behavior

[molecula451]

@pavlovcik i would assume the bots auto-assing time labeling base on what it thinks the task time would be, but i don't consider this one less than a day

[0x4007]

How long do you think this task will take? Currently we set the time estimates manually based on a guess. @rndquu what do you think on the time estimate?

[molecula451]

less than a week is approchable, but could be matched sooner

[0x4007]

As long as another core team member agrees then we can change it to Time: <1 Week! Unfortunately I am not familiar with this tech.

[molecula451]

perhaps, we could add to the bot, 2 time 1 considering and the other at last, (in less than and at last) also after a couple of weeks it looks like the bot did not unassigned the hunter

[rndquu]

This task is about a CI workflow

So in this issue we should create a workflow that runs SMT checker

There is already an almost ready PR so 1 day is enough for this issue

Fixing SMT errors will be a part of the other issue

[molecula451]

/start

[ubiquibot[bot]]

Skipping /start since the issue is closed

[molecula451]

This task is about a CI workflow

So in this issue we should create a workflow that runs SMT checker

There is already an almost ready PR so 1 day is enough for this issue

Fixing SMT errors will be a part of the other issue

The SMT it's time constrained, I'm about to open a PR, but you should already know that checking the files just for the sake of testing takes a LOT of time, and am on fast hardware

[rndquu]

This task is about a CI workflow So in this issue we should create a workflow that runs SMT checker There is already an almost ready PR so 1 day is enough for this issue Fixing SMT errors will be a part of the other issue

The SMT it's time constrained, I'm about to open a PR, but you should already know that checking the files just for the sake of testing takes a LOT of time, and am on fast hardware

a LOT of time

How long exactly?

Could you also provide the SMT log?

[molecula451]

This task is about a CI workflow So in this issue we should create a workflow that runs SMT checker There is already an almost ready PR so 1 day is enough for this issue Fixing SMT errors will be a part of the other issue

The SMT it's time constrained, I'm about to open a PR, but you should already know that checking the files just for the sake of testing takes a LOT of time, and am on fast hardware

a LOT of time

How long exactly?

Could you also provide the SMT log?

working on that

[molecula451]

This task is about a CI workflow So in this issue we should create a workflow that runs SMT checker There is already an almost ready PR so 1 day is enough for this issue Fixing SMT errors will be a part of the other issue

The SMT it's time constrained, I'm about to open a PR, but you should already know that checking the files just for the sake of testing takes a LOT of time, and am on fast hardware

a LOT of time

How long exactly?

Could you also provide the SMT log?

4 minutes to output something in just 1 contract using time, and it's not accurate, i got a good solution, but the time setback it's part of the module (SMT) there's a lot of saying in the solidity's github issues

[molecula451]

How long exactly?

Z3 building (C++) (required) by SMT https://github.com/molecula451/ubiquity-dollar/actions/runs/5316439907/jobs/9625970853 took 30 min the action to build only the dependencies. It's not suitable to use the libraries that comes with ubuntu, best it to build it, because there is hack to make it work on the compiler due to an issue they have not fixed yet, source: https://github.com/ethereum/solidity/issues/13073

Kindly extend the task label expiration

[rndquu]

How long exactly?

Z3 building (C++) (required) by SMT https://github.com/molecula451/ubiquity-dollar/actions/runs/5316439907/jobs/9625970853 took 30 min the action to build only the dependencies. It's not suitable to use the libraries that comes with ubuntu, best it to build it, because there is hack to make it work on the compiler due to an issue they have not fixed yet, source: ethereum/solidity#13073

Kindly extend the task label expiration

I don't get why we need to install Z3 solver

I thought we should simply update a foundry config and run forge build in a CI workflow

[molecula451]

I don't get why we need to install Z3 solver

This makes worth the bounty. The real reason we need Z3 Solver it's because Ubuntu ships with Z3 Binary, but not with the Z3 Headers (library) installed, required by solidity compiler to read that indeed exists and it handles the work this can be achieved by compiling the library and make install from within the compilation

I thought we should simply update a foundry config and run forge build in a CI workflow

No, it's not enough because you would get

Library installed

With the library installed you'll get actual results

You would be able to run the SMT Checker but not recursively across all the contracts

There is a machine running here with a good config to run the checker for ALL the contracts available https://github.com/molecula451/ubiquity-dollar/actions/runs/5331895073 it just clogged! for many hours, no matter in what hardware you are running, you'll mostly won't get results for over 200+ contracts recursively

I suggest we keep this task locally instead of handling it as a github action

This is a time constrained task. because of the debugging process in both compilation time && github actions time

the Z3 building takes a lot of time, like 30 minutes

a PR It's incoming get ready for this

[rndquu]

I don't get why we need to install Z3 solver

This makes worth the bounty. The real reason we need Z3 Solver it's because Ubuntu ships with Z3 Binary, but not with the Z3 Headers (library) installed, required by solidity compiler to read that indeed exists and it handles the work this can be achieved by compiling the library and make install from within the compilation

I thought we should simply update a foundry config and run forge build in a CI workflow

No, it's not enough because you would get

Library installed

With the library installed you'll get actual results

You would be able to run the SMT Checker but not recursively across all the contracts

There is a machine running here with a good config to run the checker for ALL the contracts available https://github.com/molecula451/ubiquity-dollar/actions/runs/5331895073 it just clogged! for many hours, no matter in what hardware you are running, you'll mostly won't get results for over 200+ contracts recursively

I suggest we keep this task locally instead of handling it as a github action

This is a time constrained task. because of the debugging process in both compilation time && github actions time

the Z3 building takes a lot of time, like 30 minutes

a PR It's incoming get ready for this

Could you share a CI run with the libz3.so not found error?

Perhaps we could setup a workflow with manual dispatch that checks a single contract from env variable. This way we could check all the contracts step by step. What do you think?

[molecula451]

Perhaps we could setup a workflow with manual dispatch that checks a single contract from env variable. This way we could check all the contracts step by step. What do you think?

You have one here https://github.com/molecula451/ubiquity-dollar/actions/runs/5327648976/jobs/9651321338

This CI run has the compiler error, this is a pre-defined solidity error, nothing wrong with the enviroment, it's pointing that you don't have the library to run Z3 (which it's best that other solvers, IMO)

I am rendering something, and will provide more input

[0x4007]

Thanks for your explanations molecula451. GitHub Actions can run for six hours so I don't expect timeouts to be an issue.

Job execution time - Each job in a workflow can run for up to 6 hours of execution time. If a job reaches this limit, the job is terminated and fails to complete.

[molecula451]

Thanks for your explanations molecula451. GitHub Actions can run for six hours so I don't expect timeouts to be an issue.

Job execution time - Each job in a workflow can run for up to 6 hours of execution time. If a job reaches this limit, the job is terminated and fails to complete.

Your input it's always amazing, awesome friend. Yeah it didn't last, it's too compute intensive. I dropboxed a full video here playing with the SMTChecker and the contracts

https://www.dropbox.com/s/wkgqjir8msrwxa1/full_smt.mp4?dl=0

Perhaps we could setup a workflow with manual dispatch that checks a single contract from env variable. This way we could check all the contracts step by step. What do you think?

@rndquu The SMTChecker tasks it's just too intensive for CI. because under the hood it's not only the compiler working, it is the Z3 Solver which goes down to the hardware level. We better keep this task locally

The SMTChecker it's not suitable for CI Run, there are many reasons, the Solvers are task intensive, even on fast hardware it takes a while to output checker logs. Check the video

Not all the contracts are gonna output about SMTChecker

Some contracts will just compile and that's it, even tho they were scanned using the checker

AccesControlInternal is one of them

The SMTChecker Uses all the possibles checking targets

• assert,
• constantCondition,
• divByZero,
• outOfBounds,
• overflow,
• popEmptyArray,

but it won't output results for all of em if it doesn't exists a particular issue with this in the contract, this searching is task intensive, Z3 under the hood

Don't think you won't get false positives

There are many false positives using the SMTChecker, you are in a heavy (many contracts compiling at the same tiem) computing intensive, and you'll get many falses positives? again not good for CI

Foundry has a bug with SMTChecker

it is clearly state to use show_unproved to output further results we're using show_unproved = true in our foundry config:

you still get things like:

In it's current stage this task is suitable for local use and to make it use when need it by team, when new contributions are made to the contracts, to pass the checker, but not on CI it'll be much the time/trouble that you'll dealt, than the output logs you'll need to make sure something it's good with the checker

You may deal with other Solvers

Again, to reach to this conclusion, was timely constrained and heavy compute intensive, further testing for the infrascture would be deal with other solvers, but those requires to further include 3rd party dependencies to the project

PR at https://github.com/ubiquity/ubiquity-dollar/pull/702

[ubiquibot[bot]]

[ CLAIM 600 WXDAI ]

0x4D0704f4...D826dCFc4

[molecula451]

thanks a lot awesome friends!! @pavlovcik && @rndquu