Some verif on the cache MR

We do here some verification work for the cache MR: tezos/tezos!3234 (merged)

For now, we only verify the following: the function Script_repr.micheline_nodes is equivalent to this reference definition without folding and continuations:

Reserved Notation "'micheline_nodes_list".

Fixpoint micheline_nodes {A B : Set} (node : Micheline.node A B) : int :=
  let micheline_nodes_list {A B} := 'micheline_nodes_list A B in
  match node with
  | Micheline.Int _ _ | Micheline.String _ _ | Micheline.Bytes _ _ => 1
  | Micheline.Prim _ _ subterms _ | Micheline.Seq _ subterms =>
    micheline_nodes_list subterms +i 1
  end

where "'micheline_nodes_list" :=
  (fun (A B : Set) => fix micheline_nodes_list
    (subterms : list (Micheline.node A B)) {struct subterms} : int :=
    match subterms with
    | [] => 0
    | cons n nodes => micheline_nodes n +i micheline_nodes_list nodes
    end).

Definition micheline_nodes_list {A B : Set} := 'micheline_nodes_list A B.