search

hacl-star / merkle-tree

A verified Merkle Tree, built as a standalone project on top of EverCrypt
6 stars 5 forks source link

Accessors for leaf hashes in Merkle Tree #4

Open eddyashton opened 4 years ago

eddyashton commented 4 years ago

We'd like to read individual hashes from the merkle tree, after insertion (and in fact usually after deserialisation). We're currently doing this by inspecting the tree's state directly. This is unsafe and we expect it to break each time we take an update, since we're relying on unspecified properties of the generated structs.

Can you please add some verified, generated accessors for the merkle tree state? Primarily mt_get_leaf, but ideally also mt_get_leaf_range, mt_get_begin_index, and mt_get_end_index.

msprotz commented 4 years ago

CC @fournet and @wintersteiger, for reference. Christoph, is this something you might have time for?

wintersteiger commented 4 years ago

I'm aware of the request and I think we do definitely want to add that, but I'm too busy to implement it right now. I hope I'll find some time to at least start this within a couple weeks or so.