## Blockchain-based Algorithmic Problem Solving Competitions

- Supervisor
- Asst. Prof. Eugenie Foustoucos*

- Commitee
- Asst. Prof. Spyridon Voulgaris*Assoc. Prof. Vangelis Markakis*

### Abstract

This thesis presents a blockchain-based platform where algorithmic problems can be posed as competitions, potentially, with a financial reward. A competition is won by the first individual to submit an algorithm that is both correct and bounded on time and space complexity, in accordance with the specification of the corresponding problem. Submitted algorithms must be accompanied by a formal proof of correctness which is mechanically validated by the platform. The platform is based on blockchain technology, specifically Ethereum, which ensures transparency on solution validation and allows for the automatic payment of competition rewards.

A complete system design is proposed and experimentally evaluated. The system consists of a web-based front end and a blockain-based backend. The blockain-based backend conducts competitions transparently and validates submitted algorithms and proofs mechanically. The proposed system design is evaluated by an experimental proof-of-concept implementation.

Furthermore, a theoretical setup is established in order to develop the methods and tools required to make the platform a reality. This theoretical setup includes a method for the formal specification of computational problems where problem specifications are formatted as special problem-definition algorithms. A method for proving algorithm correctness against such problem specifications is proposed based on formal program verification. A new programming language with a fully working compiler is developed for the representation of algorithms. A proof composer for proofs of algorithm correctness is developed based on a custom configuration of Hoare logic.

### 1.1.2 Concept and Actors

Competitions have two actors roles:

- Petitioner
- The individual who poses a problem and initiates a competition

- Creator
- The individual who proposes a solution accompanied by a proof

There is no role of “reviewer” as solutions are validated by the platform.

We focus on algorithmic problems, thus petitioners provide definitions of algorithmicproblems while creators provide algorithms. A definition for an algorithmic problem consist of the following:

- A definition for the underlying computational problem which will serve as a specification for the correctness of proposed algorithms
- A set of complexity constraints that must be satisfied by proposed algorithms

Creators submit algorithms in the form of a procedural program and accompany them with a proof for their correctness and their worst case asymptotic complexity. Proofs are composed with the utilization of formal program verification methods.

### 3.1.2 Competition flow

The main flow of a completion is as follows:

- The
**petitioner**submits the question*q*, initiating the competition - A
**creator**submits an answer*a*accompanied by a proof*p* - The system invokes the proof validator*
*v*on (*q*,*a*,*p*) and- if
*v*responds positively the competition**concludes successfully** - otherwise, the system allows the re-execution of
**step 2**

- if

This flow is depicted in figure 3.1.

* See Definition 3.2 of the full text for proof validators

### 3.2.2 Solver algorithms/Answer objects (simplified)

Solver algorithms/Answer objects are represented as procedural programs having the `solve`

function.

Here is an example of a solver for the natural square root of natural numbers. The result will be -1 if there is no natural square root.

### 3.2.3 Problem definitions/Question objects (simplified)

To define an algorithmic problem* we create a program necessarily containing the following funcions:

`validInstance(i)`

- Determines whether instance
`i`

is a valid instance of the problem

`negatedVerify(i, s, h)`

- Determines whether solution
`s`

is**not**correct for instance`i`

with the help of hint`h`

The `negatedVerify`

function must behave as follows:

- If
`s`

is correct for`i`

then it must return**false**for every`h`

- If
`s`

is not correct for`i`

then there must exist an`h`

for which it returns**true**

Example: Here is a definition for the natural square root problem.

This example behaves as follows:

- If
`s`

is -1, meaning there is no square root, the hint should provide the actual square root to prove the mistake - Otherwise, it compares
`s`

with the square of`i`

to check if`s`

is not the actual square root of`i`

Negating the verifier seems counter-intuitive, however, it serves for creating proofs of correctness as described in the next section.

* This page focuses on correctness, refer to the full text for details about asymptotic complexity constraints.

### 3.2.4.2 Correctness (simplified)

To examine the correctness of a given solver against a certain problem definition, we compose the program `correctness`

.

It is proved (Proposition 3.2 and section 3.2.4.2 in the full text) that a candidate solver is correct *if and only if*

- program
`correctness`

terminates for every`i`

and`h`

- and variable
`verdict`

is always`true`

at program termination.

### 4 System Design and Implementation (overview)

A petitioner must provide two inputs to create a competition:

- The problem definition
- The reward amount in eth currency

A creator needs to perform two steps to submit a solution:

- Write the solver algorithm
- Make the formal proof for the correctness of the solver algorithm against the problem definition

### 5 Evaluation (a few words)

The proof of concept system is evaluated in terms of the observed length of the proofs and the gas cost (Ethereum computational fees) required to validate them.

### 6.1 Conclusions

We have proposed a blockchain-based platform design for conducting algorithmic problem solving competitions where proposed algorithms can be mechanically validated. The feasibility of this design has been demonstrated by a proof-of-concept implementation. As part of the design, we proposed a method for representing algorithmic problem definitions as procedural computer programs and showed that these representations can be effectively used to validate the correctness and complexity bounds of proposed algorithms.

The evaluation process revealed two main issues regarding the use of the platform, though none of them is irrecoverable. The first issue arises from the length of the proofs of correctness. The relatively large number of low level deduction steps makes it cumbersome for human users to compose proofs. The second issue arises from the relatively large number of axioms needed for a proof that only relies on simple arithmetic truths. This signals that more complex proofs would require a very large number of axioms or otherwise, they would have to prove many trivial facts thus making the proofs immensely lengthy.