# Merkle Proofs

## Patricia Trees

Most of the code related to these will be found in the `lib_new_storage` library. More precisely I will refer to [simple.ml](https://gitlab.com/marigold/tezos/-/blob/ulrikstrid@rollup-rewrite-history/src/lib_new_storage/simple.ml)

A [`patricia Tree`](https://gitlab.com/marigold/tezos/-/blob/ulrikstrid@rollup-rewrite-history/src/lib_new_storage/simple.ml#L82) is a (balanced) binary tree:

 t =
  | Node of node_content
  | Leaf of leaf_content
  | Empty of empty_content

where

node_content = { left : t ; right : t ; hash : hash ; visited : bool }

leaf_content = { content : bytes 
                 hash : hash ; 
                 visited : bool }

empty_content = { visited : bool }

Note that the leaf contains content as well as a hash. The nodes will only contain a hash that is the concatenation of the left and right hashes. In particular, note that the `empty_content` has neither content nor a hash. If a node has an `Empty` child then its hash will include ``"empty"`` as the hash of that child.

### Example
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" }

and its visual representation

strict graph {
  node [margin=0 fontcolor=blue fixedsize=false shape=box style=filled]
  a [ label="emptyh1h2h3"]
  b [ label="emptyh1"]
  c [ label="h2h3"]
  e [ label="" shape=circle]
  1 [ label=" 1\n h1"]
  
  2 [ label="2\n h2"]
  3 [ label="3\nh3"]
a -- {b c}
b -- {e 1}
c -- {2 3}}

## Patricia_produce_stream

This is a module whose [signature](https://gitlab.com/marigold/tezos/-/blob/ulrikstrid@rollup-rewrite-history/src/lib_new_storage/simple.ml#L194) is:

module Patricia_produce_stream : sig
  type tt = t * stream
  val get : tt -> key -> value * tt
  val mem : tt -> key -> bool * tt
  val set : tt -> key -> value -> tt
end

Here `t` is a Patricia tree, `stream` is a list of hashes and `key` is a path, that is alist of booleans.

Assume the `t` is the tree above in [Example](#Example) and stream is the empty stream. Moreover assume `k` is the pathe [true, true] (true means take the right child). This corresponds to the picture:

strict graph {
  node [margin=0 fontcolor=blue fixedsize=false shape=box style=filled]
  a [ label="emptyh1h2h3" color="green"]
  b [ label="emptyh1"]
  c [ label="h2h3" color="green"]
  e [ label="" shape=circle]
  1 [ label=" 1\n h1"]
  
  2 [ label="2\n h2"]
  3 [ label="3\nh3" color="green"]
a -- {b c}
b -- {e 1}
c -- {2 3}}

Then the following happen:

get (t, []) k = (3, ["h3"; "C";"h3"; "h2";  "A";"h2h3"; "emptyh1";  "A"]) 
mem (t, []) k = (true, ["h3"; "C";"h3"; "h2";  "A";"h2h3"; "emptyh1";  "A"]) 
set (t, []) k 5 = (t , ["h3"; "C";"h3"; "h2";  "A";"h2h3"; "emptyh1";  "A"]) 

Note that since t already hasa value there the "set" function does nothing to the tree. However

mem (t, []) [false false]  = (false, ["C"; "h1"; "empty"; "A";"h2h3"; "emptyh1";  "A"]) 
set (t, []) [false false] "5" = (t1, ["C"; "h1"; "empty"; "A";"h2h3"; "emptyh1";  "A"]) 

where `t1` is the tree:

strict graph {
  node [margin=0 fontcolor=blue fixedsize=false shape=box style=filled]
  a [ label="ªªª5h1h2h3" color="green"]
  b [ label="ªªª5h1" color="green"]
  c [ label="h2h3" ]
  e [ label=" 5\n ªªª5" color="green"]
  1 [ label=" 1\n h1"]
  
  2 [ label="2\n h2"]
  3 [ label="3\nh3" ]
a -- {b c}
b -- {e 1}
c -- {2 3}}

Note that the stream represents the "old values" in the tree but the hashes are updated.

### The `visited` parameter.

Note that, in the above, we have excluded the discussion about the parameter `visited`. We briefly describe it here.

## Patricia_consume_stream

This is a module whose [signature](https://gitlab.com/marigold/tezos/-/blob/ulrikstrid@rollup-rewrite-history/src/lib_new_storage/simple.ml#L351) is:

module Patricia_consume_stream : sig
  type t
  type tt = t * stream
  val root_hash : hash -> t
  val get_hash : t -> hash
  val empty : t
  val get : tt -> key -> value * tt
  val mem : tt -> key -> bool * tt
  val set : tt -> key -> value -> tt
end

here `t` is a structure that is similar with the Patricia tree, execpt it is allowed to contain a hash:

type t =
    | Hash of hash
    | Full of tree

:::spoiler and `tree` is essentially a Patricia tree missing the `visited` component from the node and leaf or empty contents.

node_content = {
    left : t ;
    right : t ;
    hash : hash ;
  }

  and leaf_content = {
    content : bytes ;
    hash : bytes ;
  }

  and tree =
    | Leaf of leaf_content
    | Node of node_content
    | Empty

:::

`key` and `stream` are, as above lists of booleans respectively lists of hashes.

The operations are, in some sense, the reverse of the above with the extra note that some of the contents can just be a hash.
For example let us assume that the tree is as bellow. To save some space from clutter I will write just the tree instead of actually writing "Full tree" all the time.

We will give an extreme example, one in which

stream = ["A"; "emptyh1"; "h2h3"; "A"; "empty";"h1"; "C"; "h1"]
t = Hash "emptyh1h2h3"

We will compute (see [here](https://gitlab.com/marigold/tezos/-/blob/ulrikstrid@rollup-rewrite-history/src/lib_new_storage/simple.ml#L414))

get_opt (t, stream) [false true]

The first step will look at the key. Since it is not empty, and the t is a hash, we look inside the stream. The first element of the stream is `A` which is the `node_tag`. This means we will create a node tree. We pop the next two entries in the stream which will be the descendents of the node, they will both be "hashes". The hash of the node is the initial hash. Therefore the resulting tree in the first step is (note that we denote `Hash hash` by an oval):

strict graph {
  node [margin=0 fontcolor=blue fixedsize=false shape=box style=filled]
  a [ label="emptyh1h2h3"]
  b [ label="emptyh1" shape=oval]
  c [ label="h2h3" shape=oval]
  
a -- {b c}
}

The next step will be to look at the top of the stream to see which of the two directions we are going. Since that is `false` we will take the left path. We discard the top of stream and key and proceed in the left branch. The next step is applied to the `Hash "emptyh1"` with the stream `[]"A"; "empty";"h1"; "C"; "h1"]` and the key `[true]`. Just as before the stream starts with an `A` so it is a node. Same procedure gives:

strict graph {
  node [margin=0 fontcolor=blue fixedsize=false shape=box style=filled]
  a [ label="emptyh1h2h3"]
  b [ label="emptyh1"]
  c [ label="h2h3" shape=oval]
  e [ shape=oval label="empty"]
  1 [ label="h1" shape=oval]
 
a -- {b c}
b -- {e 1}}

Finally we look at the top of the key and see that we need to move to the righ. The final step will be done with `Hash "h1"`, the stream `["C"; "h3"]` and the empty key. Since the first element of the stream is `C`, that is a `leaf_tag` we need to make a leaf with the corresponding hash content. In particular the resulting tree will be:

strict graph {
  node [margin=0 fontcolor=blue fixedsize=false shape=box style=filled]
  a [ label="emptyh1h2h3"]
  b [ label="emptyh1"]
  c [ label="h2h3" shape=oval]
  e [ shape=oval label="empty"]
  1 [ label="h1"]
 
a -- {b c}
b -- {e 1}}

And the result will be `((Some "h1", t), [])` where `t` is the above tree.