Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Detect edge cases in contracts #833

Closed
moodmosaic opened this issue Feb 27, 2023 — with Grants Dashboard · 13 comments
Closed

Detect edge cases in contracts #833

moodmosaic opened this issue Feb 27, 2023 — with Grants Dashboard · 13 comments

Comments

@moodmosaic
Copy link

APPLICANT

Type:                                                                        Direct Application

Email:                                                                    [email protected]

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?

  • Billions have been lost to protocol exploits in 2022, more than double of 2021’s total. Most of the protocols have been audited, from the high level, but how good enough were those protocols tested for edge cases?

  • Property-based testing, fuzzing, and invariant testing are well-established techniques for testing the hard stuff and staying sane. Ethereum supports those techniques in dapp and forge. Why not having some of those features in Stacks?

  • Clarity has a LISP-like syntax. Having the option to write tests in Clarity helps you minimize context switching between two languages and focus on what matters.

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: citycoins/protocol#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
Copy link

👋 @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
Copy link

igorsyl commented Feb 27, 2023

FYI @jo-tm

@friedger
Copy link

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
Copy link
Author

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
Copy link
Contributor

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
Copy link
Contributor

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
Copy link
Contributor

@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
Copy link
Author

@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
Copy link
Contributor

Excellent! Please do. ( cc: @igorsyl )

@igorsyl
Copy link

igorsyl commented Jun 12, 2023

cc @sergey-shandar

@moodmosaic
Copy link
Author

Excellent! Please do. ( cc: @igorsyl )

@will-at-stacks, done. 👍

@moodmosaic
Copy link
Author

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

@will-corcoran
Copy link
Contributor

@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 )

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

6 participants