Free TON

DePool Contract Verification (Phase 2) [26 October 2020 — 26 November 2020]

Short Description

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

  1. Types and abstractions
  2. Contract Class to be realized during the next steps

Coq Eval/Exec specification for all public functions

  1. 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)
  2. Eval: full return values on all branches (including exceptions throwing)
  3. Exec: full state modification on all branches (in terms of contract members, including branches with exception throwing)
  4. 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

  1. Invariants (global, local etc). Here we need invariants hierarchy as well.
    1. Having Inv (S) we get Inv (S*), where S -> S*
    2. 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)
  2. Direct scenarios (functional) formulation: what we get doing smth
  3. Inverse scenarios (security) formulation: what we had done if we got smth

Review, fixes, corrections, respecification, reproving

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.

11 Likes

is there a real need to pass this through main G?

We just HAVE to change the description of this contest!

  1. 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.

  2. 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.

  3. 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.

Hope that helps.

1 Like

Yes. There is no other governance who can do this currently as we don’t have a formal verification subgov yet. May be we should. Lets discuss.

Unfortunately, this is not the answer((

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

  1. Comtetitor’s name should begin with “Pru”

  2. 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.

  1. 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.
  2. 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.

Думаю, что в текущем виде это конкурс под одного участника.
Предлагаю на выбор 3 решения:

  • увеличить срок проведения конкурса до 2-3 месяцев, чтобы нивелировать несправедливые конкурентные преимущества;
  • проголосовать за выполнение работы выбранным целевым исполнителем за награду. Без всякого конкурса;
  • сделать конкурс на выбор исполнителя, а потом выбранный выполняет работу в одиночку за награду.
4 Likes

К первому и последнему варианту: там еще надо бы индивидуально уведомить основных игроков на этом рынке

Duration of the contest should be not less 2 month.
Otherwise it is not a fair game. Smbd has 2 mnth handicap already

1 Like

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.

  1. The final version of depool contract is not published till now.
  2. 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.
  3. 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.

2 Likes

Давайте называть вещи своими именами. Если это первый грант, то давайте разработаем механизм управления грантами. Если конкурс, то сроки должны быть увеличены.

The formal verification does not relate to the contract version. The version has been published couple of months ago.

And more than that was given to anyone who wanted to participate. There will be almost 4 months from when the DePool contract was published.

No it is not but that takes into account all the time from the start of specifications work.

Above. There will be no time increase. Sorry. Next contest is coming next week. Please join.

1 Like

This proposal has been accepted by on-chain voting :point_right: https://gov.freeton.org/proposal?proposalAddress=0:9ed644435eebf731844e99cea186430159b08d43aea4d79f27e4a7871fbde698

duration in PDF - 26 October 2020 — 26 November 2020
Here, on forum - 29 October 2020 — 03 December 2020
Smth need to be corrected

1 Like