An invariant required for storage_functors.v
In file storage_functors.v we have 2 unfinished goals (admit). means we will need to add an invariant on the to_path function
https://nomadic-labs.gitlab.io/coq-tezos-of-ocaml/docs/proofs/path_encoding
admitted goals
- 0 <= I1.(INDEX.path_length) <= Pervasives.max_int
- List.z_length (to_path t []) + 1 <= Pervasives.max_int
Edited by Natasha Klaus