Contract proofs in Coq according to the specifications produced in Phase 1
Motivation
Contest submission should prove the correctness of DePool contract using Coq according to the below requirements by translating the contract code into a Coq eDSL (embedded Domain Specific Language), provide and prove Eval/Exec provide formal Scenarios description for all public functions. Issue reviews, fixes and corrections, with their subsequent reproving.
Term
Each participant should provide the following:
Translation to Coq eDSL
Types and abstractions
Contract Class to be realized during the next steps
Coq Eval/Exec specification for all public functions
Error/Value equivalence conditions, e.g. for each function the iff conditions are to be formulated when the function acts normally or throws an exception (with number)
Eval: full return values on all branches (including exceptions throwing)
Exec: full state modification on all branches (in terms of contract members, including branches with exception throwing)
Non public functions analyzing in terms if they need to be specified, or just included to correspondent public (as inlines, without additional proofs)
Proof of Eval/Exec specification
Issues review and corrections if needed, respecification and proofs
Formal specification of scenarios in terms of the already “proven functions” and state members
Invariants (global, local etc). Here we need invariants hierarchy as well.
Having Inv (S) we get Inv (S*), where S -> S*
Subclasses of invariants: value invariants (the concrete computation over the state is constant, including members themselves, as projection-like computation), predicate invariants (the concrete proposition over the state is held)
Direct scenarios (functional) formulation: what we get doing smth
Inverse scenarios (security) formulation: what we had done if we got smth
The answers should be provided in the following form:
Code equivalently mapped to the formally verifiable language (with clear indication of equivalence degree)
Standalone/separated list of statements to be proven
Requirements explicitly mentioned in the “Coq Eval/Exec specification for all public functions”
Code that proves the specification and verifiable by an external trusted proof checker (such as Coq, Agda, Isabelle, Idris, K)
The list of externally required specifications must be moved to a separate file that will allow to make a quick checkup.
Internal specifications and proofs must be provided and fully pass build chain
All the axioms (not proved assumptions) must also be moved to a separate file
Check if all the requirements mentioned above are met and provide the detailed assessment
List of notes, accepted and fixed corrections, list of rejected corrections with justification
Contest Dates:
26 October 2020 — 26 November 2020
Proposed prices:
1 place — 350,000
2 place — 250,000
3 place — 150,000
The jury:
Jury members who vote in this contest must be known experts in the field of security, smart contract audit, and formal verification.
Jurors whose team(s) intend to participate in this contest by providing submissions lose their right to vote in this contest.
Each juror will vote by rating each submission on a scale of 0 to 10 or can choose to reject it if it does not meet requirements, or they can choose to abstain from voting if they feel unqualified to judge.
Jurors will provide feedback on your submissions.
Duplicate, modifications of another submission, sub par, incomplete or inappropriate submissions will be rejected.
Jury rewards:
An amount equal to 5% of the sum total of all total tokens actually awarded to winners of this contest will be divided equally between all jurors who vote and provide feedback. Both voting and feedback are mandatory in order to collect this reward.
Procedural requirements
Because of the very specific nature of this contest only 1 submission per team is acceptable. Submissions should not be a modified version of another submission. Jury should take special care in reviewing submissions in that respect.
All submissions must be accessible for the jury to open and view, so please double-check your submission. If the submission is inaccessible or does not fit the criteria described, the submission may be rejected by jurors.
Contestants must submit their work before the closing of the filing of submissions. If not submitted on time, the submission will not count.
All submissions must contain the contestant’s contact information, preferably a Telegram ID by which jurors can verify that the submission belongs to the individual who submitted it. If not, your submission may be rejected.
If your submission has links to the work performed, the content of those links must have the contestant’s contact details, preferably a Telegram ID so jurors can match it and verify who the work belongs to. If not, your submission may be rejected.
Disclaimer
Anyone can participate, but Free TON cannot distribute tokens to US citizens or US entities.
We just HAVE to change the description of this contest!
In the initial contest (phase 1), there were no conditions for mandatory usage of the specification of the winner of the phase 1 in further contests. When developing requirements for phase 2, the results of work on phase 1 should be indicated as OPTIONAL additional materials/documents.
The purpose of this competition is to formally verify the correctness of the DePool contract. That’s all. The remaining words in the “Motivation” section are harmful to achieving the goal and limit competition and the tools used for formal verification.
There are different approaches and tools for formal verification of code and developing deduction trees (please see list of tools in the linked article below).
And it’s not just Coq! Links to specific tools should be excluded from the contest description.
This is not that simple unfortunately for few reasons:
The formal verification contest was designed as a 3 stages contest. If on Stage 1 there would be any indication that someone may participate with alternative verification technics — the phase 2 would take that into account. As far as I remember there were none. No other specification was provided.
Unlike most of the contest the Phased contests are such because all phases are together form the solution. Specifications are important part of the verification. Therefore if you did not submit the Specifications on the first Phase you should either use the one submitted or submit another as part of the second Phase which would be formally incorrect. Which leaves us with only one option: the one that is reflected in the current proposal.
Hope that answers it.
On a more general note:
There will be lots of formal verification contests going forward. If you want to participate with another prover — you are more than welcome. But please consider also this:
Formal verification is extremely hard.
Very few teams can actually perform it in the world.
Free TON from the start has announced its support for Coq long term. This is our technical vision.
There was no opposition or alternative presented.
It is important that we focus on something we can actively support as a community and where Free TON will have an edge over other blockchains. I believe our expertise in Coq is our very strong advantage that brings a lot of value to the network.
You can desing any contest with any number of stages, but you should transparently define the rules of the entire chain of contests at the first stage. This was not done. At the moment, the description of the contest looks like an imposition of technology, and this is completely wrong. If you want to follow this way, then add the following requirements to the competition (because this is closely related with the logic of your answer):
Comtetitor’s name should begin with “Pru”
Comtetitor’s name should end with “vendo”
Next stage on this way will be direct financing. Let’s go!
I want to immediately apologize for some of the sarcasm above and of course I have great respect for the activities of the company whose name I inadvertently mentioned in my sarcastic example above.
Do you want to participate or know anyone who would like to participate with another prover? Lets ask it right now right here: if anyone would like to participate with another prover please write a comment below.
Coq is one of the most established provers on the market. The other real option is K (and even that is not certain). So theoretically you have many proof assistants but practically you don’t and it is definitely nor equal Pruvendo as they are not the only team in the world specializing in Coq. Your sarcastic statement therefore is also an incorrect one.
This means only that the contest prizes must be attractive enough for those professionals to participate, thus making this contest look like an invitation to tender which [probably] must be considered a special type of contest with [potentially] custom rules.
Aren’t they already?
And this is NOT a tender as we consider only working solutions. There is a big difference. I expressed my personal view many times over on that point.
Ok, if we really need speed, I see only one honest way:
we determine the due date, the reward and vote for the performance of the work by the selected performer. Without any competition. Then we vote whether the working solution was provided by the performer or not (i.e. whether he should receive reward).
We can not do that and I also think we should not. If there is a team out there that wants to participate — they could. The DePool contract as well as specifications were published months ago. There was no problem to prepare. The full month is more than enough to finalize according to the above specs.
The final version of depool contract is not published till now.
On today’s youtube stream, you explain us that FV is a lot-lot-lot works, so many works, that special company doing it 3 months still does not finished it.
You write that 5 weeks is quite enough for such work.
Where is Truth, brother? :))
P.S. I would like to ask to increase time of the contest up to 8-10 weeks, after depool final version will come to public.
Давайте называть вещи своими именами. Если это первый грант, то давайте разработаем механизм управления грантами. Если конкурс, то сроки должны быть увеличены.
