Christoph M. Wintersteiger
Christoph M. Wintersteiger
Good to see PRs are now required! This changes the vectors in Merkle tree deserialization to have a reserved size of 0, to circumvent https://github.com/FStarLang/FStar/issues/2072, so CCF can upgrade their...
We're seeing a bunch of memory leaks in CCF again. I think it was 9fb8ae67554ad21bdf56277bb2b5afe3d7f82417 and the following snapshot in 1cf6f496a347b8740be8caf4af96b7c66fbd87f6, which removed `KRML_HOST_FREE(s);` from `EverCrypt_Hash_free`, so the state objects...
For a proper CCF release, we need a proper EverCrypt release, i.e. a named release with a version number we can refer to, instead of a git hash. Are there...
After seeing memory leaks after an upgrade to the latest hacl-star, I think it would be helpful to enable the clang address sanitizer (or similar) in the CI builds/tests. Did...
Yes, I know about `NODEPEND=1`, still, this seems a bit excessive... ``` [FSTAR-DEPEND (make)], 0:41.34 [FSTAR-DEPEND (full)], 0:53.41 [VALE-DEPEND], 2:26.91 ... [FSTAR-DEPEND (make)], 0:40.31 [FSTAR-DEPEND (full)], 0:52.47 [VALE-DEPEND], 2:26.39 ```...
We have a use-case for which we need Merkle path serialization. We should really add to our interface next to whole-tree serialization. (I'll probably add it myself some time soon.)
Not intended to be merged as is, just a demo to show that it doesn't take all that much. I just ran `CROSS=yes make` and, on a proper Ubuntu machine...
Kremlin often renumbers function parameters when it's not really necessary (or at least not obvious why it is necessary). For instance, `i1` on `mt_create` here: https://github.com/project-everest/hacl-star/blob/3cc6ce0ce91ce41fddb328aa809df234e6185eff/dist/gcc64-only/MerkleTree.h#L95
Removing the `inline_for_extraction` from `hcpy` here: https://github.com/project-everest/hacl-star/blob/cwinter_merkle_hashes/secure_api/merkle_tree/MerkleTree.Low.Datastructures.fst#L189 makes kremlin produce `(hcpy(hsz), (void*)0)` instead of `hcpy(hsz)`, i.e. the result is overwritten by a null pointer.
Quick one before I forget: I think it would make sense to add a clear notice to the kremlib files explaining that the code contained therein is not verified.