# Lib_traced_storage

Most of the code related to these will be found in the `lib_traced_storage` library.

## Hashes

A hash is an abstract type that is under the hood just bytes. It does, however, expose the following functions:

  val empty : t

  val to_bytes : t -> bytes

  val digest : bytes -> t

  val digest_couple : t -> t -> t

  val of_bytes_exn : bytes -> t

  val of_bytes_opt : bytes -> t option

allowing one to go back and forth beween bytes and `t` and to concat two hashes.
## Keys

A key will be a sequence of booleans reresenting a path in a binary tree. A key can be transformed back and forth from bytes and strings. that is

key_to_string [ true; false; false] = "100"

## Common

This is the "common" type in the library. It has signature:

type t
type nonrec key = Key.t
type nonrec value = bytes
val get_opt : t -> key -> t * value option
val get : t -> key -> t * value
val mem : t -> key -> t * bool
val set : t -> key -> value -> t

I will describe the implementation for each of these.

## Tree

This is the commons tree structure. Each of the modules bellow will implement this structure, possibly with some extra decoration.

  and t =
    | Node of node_content
    | Extender of extender_content
    | Leaf of {content : bytes; hash : Hash.t}
    | Empty

and

  type node_content = {left : t; right : t; hash : Hash.t}

  and extender_content = {node : t; hash : Hash.t; key : Key.t}

It will also have some functions that allow for hashing.

Note that the leaf contains content as well as a hash. The nodes will only contain a hash that is the hash of the concatenation of the left and right hashes.
An extender will be a compact representation of an `empty` path. More precisely, the tree

strict graph {
  node [margin=0 fontcolor=blue fixedsize=false shape=box style=filled]
  0 [ label=" emptyemptyeemptya " ]
  00 [ label="" shape=circle]
  01 [ label=" emptyeemptya "]
  010 [ label="" shape=circle]
  011 [ label=" emptya " ]
  0110 [ label="" shape=circle]
  0111 [ label="a" ]

  
 
0 -- {01 00}
01 -- {011 010}
011 -- {0110 0111}

}

which should be represented by:

 Node {left = Empty;
       right = Node
                {left = Empty;
                 right = Node
                          {left = Empty;
                           right = Leaf
                                    {content = "a";
                                     hash = "a"};
                          hash = "emptyab"};
                 hash = "emptyemptyab"}; 
       hash = "emptyemptyemptyab"}

will be represented by

Extender {node = Leaf a; 
          key = [true; true; true];
          hash = "a111"}

There will be three invariants that we need:
1. No `Node` can contain an empty child. That is

  Node {left = Empty; right = node ; hash = "empty"^h}

should be replaced by

Extender {key =[true]; node ; hash = "h1"}

2. No extender should contain an extender as a node. More precisely

Extender {key = key1; 
          node = 
               Extender {key = key2; node ; hash = "h"@key2}; 
        hash = "h"^key2^key1}

Should be replaced by

Extender {key = key1 @ key2; 
          node; 
          hash = "h"^(key1@key2)}
          

As a consequence of this, `Empty` in the empty tree or at the end of an `Extender`. We also want

3. No extender should en in `Empty`. If it does it should be replaced by `Empty`.

None of the 3 invariants are enforced in code but they cannot apper as consequences of `set`. If, later on we would want to remove values form leaves we will want to take care that these remain true. There are PBT tests checking these. Moreover there is some atavic code dealing with empty extenders just in case.

the Patricia trees are meant to be representations of `(key,value)` pairs. In particular one can get the value corrsponding with a key respectively set the value at a certain key.

## Patricia

### Getting values:

Given a key `k`, trying to `get tree k` will return:

1. `Failure` in the following two cases:
* The path corresponding to `k` continues pass a Leaf.
* The path corrsponding to `k` finishes either on a node or in the `middle` of an extender.

2. `None` if one of the two happen:
* The path corresponding to `k` continues past an empty.
* The path corresponding to `k` diverges from the path corrsponding to the key inside of an extender.
3. `Some a` if the path corrsponding to `k` ends on a Leaf whose content is `a`
### Examples:
Let us consider the following tree:

strict graph {
  node [margin=0 fontcolor=blue fixedsize=false shape=box style=filled]
  0 [ label="extender\n key = 101"; shape=oval ]
  
  01 [ label="ab"; shape =diamond]
  010 [ label="a"]
  011 [ label=" b "]
0 -- {01}
01 -- {011 010}
}

Then `get tree path` gives:
* Failure if `path = 10, 101,10111, 10100,10100001` etc.

* `None if` `path =10000, 1100,11111` etc.

* `Some a` if `path = 1010` and `Some b` if `path = 1011`

### Setting values:
Given a key `k` and a value `val`, trying to `set tree k val` will return:

1. `Failure` in the following two cases:
* The path corresponding to `k` continues pass a Leaf.
* The path corrsponding to `k` finishes either on a node or in the `middle` of an extender.
2. If the path corrsponding to `k` ends on a Leaf or an empty, then we replace this last node with a leaf whose conent is `val`.
3. If the path corresponding to `k` continues past an empty, then one replaces the empty with an extender whose key is the remainder of `k` and whose node is leaf with content `value` as its node.
4. If the path corresponding to `k` diverges from the path corresponding to the key inside of an extender then we split the extender at that position and introduce a node with a dangling extender.

### Examples
Let us consider the following tree:

strict graph {
  node [margin=0 fontcolor=blue fixedsize=false shape=box style=filled]
  0 [ label="extender\n key = 101"; shape=oval ]
  
  01 [ label="ab"; shape =diamond]
  010 [ label="a"]
  011 [ label=" b "]
0 -- {01}
01 -- {011 010}
}

then
* `set tree path val` will fail if path = 1, 10, 101, 1010000` etc.
* `set tree path "c"` where `path = 1110` gives:

strict graph {
  node [margin=0 fontcolor=blue fixedsize=false shape=box style=filled]
  0 [ label="extender\n key = 1"; shape=oval ]
  00 [ label="ab"; shape =diamond]
  01 [ label="ab"; shape =diamond]
  000 [ label="extender\n key = 110"; shape=oval]
  0000 [ label="c"]
  010 [ label="a"]
  011 [ label=" b "]
0 -- { 00}
00 --{000 01}
000 --{0000}
01 -- {011 010}
}

* `set tree path "c"` where `path = 1010` gives:

strict graph {
  node [margin=0 fontcolor=blue fixedsize=false shape=box style=filled]
  0 [ label="extender\n key = 101"; shape=oval ]
  
  01 [ label="ab"; shape =diamond]
  010 [ label="c"]
  011 [ label=" b "]
0 -- {01}
01 -- {011 010}
}

For example consider the following valid tree (I will remove the visted as it is a technicality used in constructuctions. See [this](#The-visited-parameter) for some details):

Node {left = Node {left = Empty ; 
                   right = Leaf {content = "1"; hash = "h1"};
                   hash = "emptyh1";
                   }
      right = Node {left = Leaf {content = "2"; hash = "h2"};
                    right = Leaf {content = "1"; hash = "h1"};
                    hash = "h2h3";};
      hash ="emptyh1h2h3" }

## Streams

There are two types of streams, `Stream_produce.t` and `Stream_consume.t`. The types are abstract but, behind the hood they are lists of stream elements, that is elements of type:

type stream_el =
  | Empty
  | Leaf of Bytes.t
  | Node of Hash.t * Hash.t
  | Extender of Hash.t * Key.t

They are meant to be a compact representation of traversing a piece of the tree.

`Stream_produce` has access to a function that `produce` of type `:t-> stream_el ->t` , (a function that adds a stream element to the stream) and to a function `to_consume` of type `:t-> Stream_consume.t`. In practice, produce preappends the stream element to the list and `to_consume` reverses the stream. There is also an encoding function.

`Stream_consume` has acces to an encoding function and to a `consume` function of type `t -> stream_el * t`. In practice the latter splits the head form the tail of the list.

## Patricia_Produce
This is the type that produces proofs for gets and sets. Its main type will contain a tree and a stream (the proof):

t = tree * Stream_produce.t

where

tree = {tree : VTree.tree; visited : bool}

and `VTree.tree` is a tree as above.

It also has methods for `get` and `set`. The result will be similar with above but, in addition, the functions will also add to stream. The stream will encode the nodes it has encountered in the path. The visited tag avoids overly eager streaming. The point of this is that a Stream_produce stream will be consumed in Patricia_consume allowing one to recover the important parts of the tree form just the root_hash, hence verifying proofs. The fact that a node has been visited means that it is aleady unfolded in the consumend part so you do not need to write again. Here is a simple example. Suppose $t$ is the following tree. We will color green to mean visited. Initially there are no visited nodes.

strict graph {
  node [margin=0 fontcolor=blue fixedsize=false shape=box style=filled]
  0 [ label="extender\n key = 101"; shape=oval ]
  
  ab [ label="cdb"; shape =diamond]
  cd [ label="cd"]
  b [ label=" b "]
0 -- {ab}
ab -- {cd b}
cd -- {c  d}
}

We now do

get (t, Stream_produce.empty) 1011 = ((t', stream), Some b)

where `t' = {tree, visited=true}` is the following tree:

strict graph {
  node [margin=0 fontcolor=blue fixedsize=false shape=box style=filled]
  0 [ label="extender\n key = 101"; shape=oval; color=green]
  
  ab [ label="cdb"; shape =diamond; color=green]
  cd [ label="cd" ]
  b [ label=" b "; color=green]
  c []
0 -- {ab}
ab -- {cd b}
cd -- {c  d}
}

and

stream = [Leaf "b";
          Node ("cd", "b"); 
          Extender ("101", "cdb")]

Now if we apply

get (t', stream) 10101 = ((t'', stream''), Some d)

Here t'' is

strict graph {
  node [margin=0 fontcolor=blue fixedsize=false shape=box style=filled]
  0 [ label="extender\n key = 101"; shape=oval; color=green]
  
  ab [ label="cdb"; shape =diamond; color=green]
  cd [ label="cd" ; color=green]
  b [ label=" b "color=green]
  c []
   d [color=green]
0 -- {ab}
ab -- {cd b}
cd -- {c  d}
}

and

and

stream = [Leaf "d";
          Node ("c", "d");
          Leaf "b";          
          Node ("cd", "b"); 
          Extender ("101", "cdb")]

Note that only the last two steps were added to the stream. We will see how this is consumed in teh next section.

## Patricia_consume

This is the main type that is exposed to the protocol. It is the verifier type. As before, its type will be `tree * stream` where stream is a `Stream_consume.t` while tree has type

 type tree =  Hash of Hash.t 
            | Full of tree_view

and `tree_view` is essentially a `Tree.t`. The point is that `Hash h` represents the root_hash of a subtree. Apllying the `get` respectively `set` not only finds the value but also verifies the proofs. For example let assume that we are trying the examples from the Patricia_produce. Suppose we have the reverse of the final stream in that example.

stream = [Extender ("101", "cdb");
          Node ("cd", "b");
          Leaf "b";
          Node ("c", "d");
          Leaf "d"]

if we apply

get (Hash "cdb101", stream) 1011 = ((t', stream'), Some b)

where t' is the tree (we use circle hor a hash node):

strict graph {
  node [margin=0 fontcolor=blue fixedsize=false shape=box style=filled]
  0 [ label="extender\n key = 101"; shape=oval]
  
  ab [ label="cdb"; shape =diamond]
  cd [ label=" Hash cd " shape=circle]
  b [ label="b"]
 
0 -- {ab}
ab -- {cd b}

}

and of course

stream' = [Node ("c", "d");
           Leaf "d"]

The point is that `consume_stream stream tree` does not consume the stream in the case when `tree` is of type `Full t` but only in the case of `Hash h`. Therefore applying

get (t', stream') 10101 = ((t'', []), Some d)

where `t''` is almost the initial tree (the `Leaf c` is still a `Hash`):

strict graph {
  node [margin=0 fontcolor=blue fixedsize=false shape=box style=filled]
  0 [ label="extender\n key = 101"; shape=oval ]
  
  ab [ label="cdb"; shape =diamond]
  cd [ label="cd"]
  b [ label=" b "]
  c [shape=circle label=" Hash c "]
0 -- {ab}
ab -- {cd b}
cd -- {c  d}
}