verse-lab / toychain Goto Github PK

Generally, we can't prove general injectivity of the hash functions used in current cryptocurrencies. This makes it impossible to fully instantiate Toychain for e.g., Bitcoin and Ethereum. However, there may be some way to weaken the injectivity requirements to something along the lines of "absence of collisions" and retain currently proved network invariants.

To allow behavior consistent with PoW protocols such as Bitcoin, we need to call the VAF function when receiving a BlockMsg. The most straightforward solution to me appeared to be changing:

| BlockMsg b =>
  let: newBt := btExtend bt b in
  let: newPool := [seq t <- pool | txValid t (btChain newBt)] in
  let: ownHashes := dom newBt ++ [seq hashT t | t <- newPool] in
  pair (Node n prs newBt newPool) (emitBroadcast n prs (InvMsg ownHashes))

into:

| BlockMsg b =>
  if VAF (proof b) ts (btChain bt) (txs b) then
    let: newBt := btExtend bt b in
    let: newPool := [seq t <- pool | txValid t (btChain newBt)] in
    let: ownHashes := dom newBt ++ [seq hashT t | t <- newPool] in
    pair (Node n prs newBt newPool) (emitBroadcast n prs (InvMsg ownHashes))
  else
    pair st emitZero

in Protocol.v.

However, this leads to problems in the proof of the key lemma clique_inv_step, whose type is defined in terms of the functions blocksFor and msg_block, which implicitly express that all sent blocks will be included in the forest in each node, regardless of whether VAF returns true or not.

A straightforward solution to me seems to be to change msg_block and blocksFor to the following:

Definition msg_block (msg : Message) (bt: BlockTree) (ts : Timestamp) : block :=    
if msg is BlockMsg b then
  if VAF (proof b) ts (btChain bt) (txs b) then b
  else GenesisBlock
else GenesisBlock.

Definition blocksFor n ms bt ts :=
  [seq msg_block (msg p) bt ts | p <- ms & dst p == n].

and to adjust clique_inv properly:

(* Relating global and local block-trees *)
   forall n', holds n' w (fun st => bt = foldl btExtend (blockTree st) (blocksFor n' (inFlightMsgs w) (blockTree st) ts))

However, I cannot see a way to prove clique_inv_step without making the outcome of VAF invariant in some way across timestamps. One way to accomplish this is to make Timestamp an ordType and adding an axiom saying that VAF is preserved under the ordering:

Axiom VAF_ord :
  forall (b : block) bc ts ts',
    ord ts ts' ->
    VAF (proof b) ts bc (txs b) -> 
    VAF (proof b) ts' bc (txs b).

That is, once VAF is true at some point, it continues to be true for future points in time. But I am unsure how this meshes with contemporary proof-of-stake protocols (Bitcoin doesn't care about timestamps). Could either of you comment @ilyasergey @dranov?

Currently, key functions and properties are naked global Parameter and Axiom declarations. This makes it inconvenient to create multiple instances of Toychain for different applications, and check that they fulfill all (or most) of the requirements. Ideally, there would be a mathcomp-style type with a convenient mixin for this purpose. My current minimum-effort workaround is to define a functor, which does not fit well with the general project organization.

MathComp, being designed for specification and proofs, is known to generate inefficient and bloated OCaml code during extraction. One way to get clean and efficient code is to refine Coq functions and datatypes using the approach from CoqEAL, as described in the paper Refinements for Free!.

Instead of maintaining a fork of the Hoare Type Theory (HTT) library, depend on a release of the library in the same way as depending on ssreflect (e.g., via OPAM). I have submitted a pull request that makes HTT more packaging friendly as a first step.

Once there is some way to create instances of Toychain (e.g., Bitcoin, Ethereum), it may be worthwhile to package Toychain as a library others can depend on, and even submit an OPAM package to the Coq OPAM repository. This would reasonably require that the HTT library is packaged properly as well.

Hi folks!

Happy new year!

I've just noticed toychain does not compile with dev mathcomp (and coq dev, but changes are from ssreflect path's library). It is a very quick fix ( germanD@935b73dab66ef6304252cd2a307e769b37ee7bddl). Shall I open a MR? Or you are planning updates in the future?

The Address and nid types are both defined as aliases of nat. This is fine as far as it goes, but they seem also to be used as if they always are in fact the same type. For example, we have

Parameter genProof : Address -> Blockchain -> option VProof.

But the genProof function is then used in the procInt function as follows:

let: attempt := genProof n bc in

where n is nominally of type nid.

Wouldn't it make more sense to let Address be an arbitrary Type, eqType, or ordType? That Address and nid are really the same type here seems accidental and restrictive for anyone implementing genProof. Another solution that at least makes things clearer is to explicitly assign nid to be Address or eliminate nid altogether.