-
Notifications
You must be signed in to change notification settings - Fork 12
Extraction
In the following section I will discuss the developments to the project in the extraction branch and what still needs to be done.
Compared to master the extraction branch has been refactored slightly and has few additional files.
This folder contains two additional files compared to the master branch, these are:
Parameters.vCanonicals.v
This file contains all the types that needed to be defined before extraction due to the fact that they are of type ordType/finType/eqType which causes them to extract as:
let example = exampleImplementation
however because these are types they should be:
type example = exampleImplementation
If this either isn't an issue or can be remedied another way, it would offer more implementation flexibility. However the flip side is that it decreases the size of the trusted codebase.
This file just contains all the other parameters taken from the Forests.v file that need to be realised either during extraction or extracted to a defined value in OCaml. Originally these parameters were refactored out of the Forests.v file because the idea was to define some of them in Coq, thus the separate file would allow for tidier code. Although this is now not the case it was left as is for the same reason.
Small code changes have also been made throughout the file compared to the equivalent sections in the Forests.v file in master. These changes are of the form:
exampleType --> [someType of exampleType] or exampleType_someType where someType is eqType, finType, ordType etc.
All the parameters have been removed from this file however the rest of the file is the same.
Only minor changes in this folder. Mainly adding the dependencies to the Canonicals.v and Parameters.v file however some other small changes were made.
On line 12, the definition for Address_ordMixin was changed from fin_ordMixin Address to fin_ordMixin Address_finType. In similar fashion the definition of initState was changed to use [ordType of Address].
These changes were made to fix type errors upon compilation.
For the same reason as in States.v, Address was changed on lines 92, 93, and 94 to Address_ordType.
This folder contains two sections, the Extraction.v file in the main folder and the Extracted sub-folder in which all the extracted files are put.
Require Import ExtrOcamlBasic ExtrOcamlString. this line is needed to extract certain Coq primitives to OCaml correctly.
Extraction Inline ssrbool.SimplPred. this line solves an issue where the implementation of the extracted ssrbool.ml does not match the interface. The same line is used in the DiSel project to address the same issue.
Extract Constant someIdentifier => "Something.example". This line extracts someIdentifier as Something.example in the OCaml code.
Extract Inlined Constant someIdentifier => "Something.example". Some of the parameters were extracted like this because a similar implementation - interface mismatch error occurred when trying to build.
Separate Extraction procMsg procInt initWorld. This line recursively extracts the functions procMsg, procInt, initWorld and places the dependencies in separate files, instead of one large file.
This file contains the hashT and hashB functions. Originally the hash functions were also in the Implementations.ml file however they needed to be separated to remove circular dependencies.
hashT currently uses the Hashtbl.hash function to hash a transaction and returns a string of the hash.
hashB does much the same as hashT however if the block has a prevBlockHash of 0000000 it returns "0000000".
This file implements many of the functions that needed to be realised from the Parameters.v file. Some are trivially implemented at the moment but the ones that may require a little explanation are mkProof and fcr.
mkProof makes a tuple of the inputs and computes a hash of them. This hash is then compared against a randomly generated number. If the hash is larger then the proof tuple is returned, else None is returned.
fcr compares the hashes of two blockchains returning true if the first blockchain inputted has a larger hash.
The following files haven't been linked to the build yet because all issues with the extracted code (such as realisation of axioms) needs to be dealt with. To integrate it these files into the build would just require amending the types (such as address) used to the nearly isomorphic types in the extracted code.
Runner.mlWrappers.mlShim.ml
This file contains the high level function node_run and its helper function aux. node_run is just a driver function for the node. It calls the required send or receive wrapper functions.
This file contains the two main wrapper functions responsible for sending or receiving packets:
send_action_wrappertryrecv_action_wrapper
send_action_wrapper is currently pretty much an empty wrapper, but it was kept due to the flexibility it gives if additional actions need to be made when sending a packet.
tryrecv_action_wrapper is a more complex function. It first checks for new connections and afterwards gathers all file descriptors, including any new ones. select is used to get those file descriptors that are ready for reading, these packets are then read (if possible).
This file contains the lower level Unix operations that need to be handled to perform networking operations. However, this file will need to be amended slightly to use extracted types and functions instead of the dummy ones currently used. A clear example of this would the lstate instead of coq_State. A lot of the functions names are reasonably descriptive in what the respective function does, however for some functions more information is given below.
setup sets up a socket on a node that this node is listening on.
send_chunk and receive_chunck are the lowest level functions dealing with like their name suggests, relaying buffers.
send_packet and recv_packet appropriately marshals or un-marshals packets and uses send_chunk or receive_chunck to relay.
recv_msg is slightly higher level function which takes a received packet and appropriately processes the message depending on it's type. When the shim is fully integrated this function (and its auxiliary functions) may disappear due to the overlap with procMsg however it might still be needed to perform auxiliary tasks.
recv_or_close does not actually close the connection on a socket but rather assumes the socket on the other side has been closed.
check_for_new_connections and new_conn work together, and are called every time a node wants to receive packets. This is done because connections from new sockets need to be accept'ed otherwise these packets will not be received.