hacl-star icon indicating copy to clipboard operation
hacl-star copied to clipboard

Accessors for leaf hashes in Merkle Tree

Open eddyashton opened this issue 4 years ago • 2 comments

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.

eddyashton avatar Jul 09 '20 09:07 eddyashton

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

msprotz avatar Jul 09 '20 20:07 msprotz

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.

wintersteiger avatar Jul 10 '20 12:07 wintersteiger