search

stacksgov / grants-program

Welcome to the Stacks Foundation Grant Program. Community members interested in submitting a grant proposal may do so by opening an issue in this repository and filling out the grant application.
141 stars 36 forks source link

Detect edge cases in contracts #833

Closed moodmosaic closed 1 year ago

moodmosaic commented 1 year ago

APPLICANT

Type:                                                                        Direct Application

Email:                                                                    nikos.baxevains@gmail.com

Discord:                                                    moodmosaic#6537

Twitter:                                                        nikosbaxevanis

Stacks Forum:           

GRANT BASICS

Grant Name:                                        Detect edge cases in contracts

Total Budget:                              151,200

Total Duration:                 2,160

Grant Type:                                               Stacks Foundation Direct Investment

Grant Track:                                          Stacks Developer Experience

Grant Goal:                                               Integrate Between Technologies

Grant Audience:             Developers

Specific Audience:         Stacks devs working with Clarinet, keen to learn advanced testing techniques.

Grant Team:                                       @moodmosaic

Previous Grants:                      

Ecosystem Programs:      

GRANT MISSION, IMPACT, RISKS & REFERENCE

Grant Mission:         Pandora is essentially a set of articles, example source code, and a forked version of Clarinet, that makes it easier for us, the Stacks developers, to detect edge cases in Clarity contracts.

Pandora enables property-based testing, fuzzing, and invariant testing for smart contracts that run on the Stacks 2.x layer-1 blockchain.

Pandora discovers and run tests written in Clarity and TypeScript.

Pandora is backwards compatible with Clarinet; your existing Clarinet tests can–and should–co-exist with property-based ones.

Why?

Grant Impact:               It can be possible to use these techniques and detect edge cases in already deployed contracts. It can also be possible to use these techniques to improve existing testing structure as I briefly discuss here: https://github.com/citycoins/protocol/issues/3

Grant Risks:                          Depending on the roadmap of Clarinet, you might end up having two complementary tools; Clarinet for contract development, deployments, and testing, and a forked version of Clarinet for contract fuzzing. Though the ideal scenario is to contribute this work to Clarinet.

Support Link:                                     On-going article series about the idea and the techniques. Other places were I have discussed about this are:

GRANT ROADMAP & DELIVERABLES

MILESTONE 1:

Deliverable:                   Series of articles acting as documentation and overall context.

MILESTONE 2:

Deliverable:                   Example source code on advanced testing techniques in TypeScript.

MILESTONE 3:

Deliverable:                   A modified version of Clarinet with support for writing tests in Clarity.

MILESTONE 4:

Deliverable:                   Fuzzing Clarity contracts from TypeScript.

MILESTONE 5:

Deliverable:                   Fuzzing Clarity contracts from Clarity itself.

MILESTONE 6:

Deliverable:                   A modified version of Clarinet running both TypeScript and Clarity tests.

FINAL DELIVERABLE

Deliverable:                   A modified version of Clarinet supporting advanced testing techniques.

stacks-foundation commented 1 year ago

👋 @moodmosaic
Thanks for your application! We will do a pre-review and let you know if we have any immediate questions. In the mean time please refer to our review schedule here for a detailed timeline and response dates.
Best, Will

igorsyl commented 1 year ago

FYI @jo-tm

friedger commented 1 year ago

I like better tests. Can we make use of the non-turing completeness? And go towards formal verification?

This grant is work of 1 year full time?

We can already write test with clarinet in clarity. What would be the difference to the current state?

moodmosaic commented 1 year ago

Can we make use of the non-turing completeness? And go towards formal verification?

Do you mean symbolic execution? This would be nice to have, and orthogonal to the proposed property-based/fuzzing feature:

type type arguments semantics
concrete test no single execution with concrete values (you are here)
property test yes multiple executions with randomly generated concrete values (smaller values)
fuzz test yes multiple executions with randomly generated concrete values (biased)*
symbolic test optional exhaustive exploration of all possible execution paths (what you propose)

property and fuzz is what is proposed with this grant application.

Do you expect Stacks developers to jump from concrete to symbolic without first adding property and fuzz tests? I'd be interested to have your thoughts on this.

This grant is work of 1 year full time?

It could be, yes. It depends on the date it will officially start (if it ever starts).

We can already write test with clarinet in clarity.

AFAICT, we can write tests in TypeScript that are then run via deno using Clarinet, or run via node in other tools that are similar to Clarinet, but I'm not aware of a tool that allows you to write tests in Clarity itself, and have those tests also run as property-tests, check the contract's invariants and detect edge-cases. /cc @lgalabru

What would be the difference to the current state?

I believe that the above already answers this question, but I'm happy to provide more details and context. Thank you for your input. 👍

will-corcoran commented 1 year ago

Hi @moodmosaic

Thanks so much for this application. Sounds like a fantastic tool and glad to see you got the attention of @friedger and @igorsyl . That said, we are going to deny your application now as we are laser focused on funding sBTC related work. I would ask that you consider re-applying in Q3 of this year once protocol-level blockers related to sBTC are addressed. Please note that we will be posting several sBTC-related Critical Bounties in the coming weeks here. Please keep your eyes peeled and submit an application to complete a bounty if any of them jump out at you.

Best, Will

whoabuddy commented 1 year ago

Will add that @moodmosaic is an amazing resource for testing and extremely knowledgeable on the subject. Adding to some of the work listed in the application, he also explored adding fuzz techniques to Clarinet with a few well-defined examples.

This type of tool would be a powerful resource for developers, and I definitely encourage @moodmosaic to apply again in Q3.

Also wanted to note that in the original version of PoX-Lite or "poxl" Jude's preferred approach was testing Clarity with Clarity via clairty-cli. The patterns there may be useful to you per your comment here!

will-corcoran commented 1 year ago

@moodmosaic

Not sure if you saw, but we have a new batch of RFPs open and we would love for you to apply again. We feel your smart contract edge detection project could fit in well. Please go to grants.stacks.org for more information.

Best, Will

moodmosaic commented 1 year ago

@will-at-stacks Thank you. I am thrilled about the prospect of contributing to and learning from this distinguished community. I am catching up on the discussions around sBTC testing. If I am up to speed by the deadline date (6.20.2023), I may apply.

will-corcoran commented 1 year ago

Excellent! Please do. ( cc: @igorsyl )

igorsyl commented 1 year ago

cc @sergey-shandar

moodmosaic commented 1 year ago

Excellent! Please do. ( cc: @igorsyl )

@will-at-stacks, done. 👍

moodmosaic commented 1 year ago

@will-at-stacks, I submitted a few days ago but I didn't receive a confirmation (yet).

will-corcoran commented 1 year ago

@moodmosaic can you please provide a link to your resume? the link you pasted in the application was to this post - not an actual CV. thanks

( cc: @igorsyl )