Revision 539576ec53104316dacac738fca7bc8fd967de62 authored by Son Ho on 26 February 2021, 12:56:35 UTC, committed by Son Ho on 26 February 2021, 12:56:35 UTC
generate the target architecture #define
1 parent 7fc6186
MerkleTree.h
/* MIT License
*
* Copyright (c) 2016-2020 INRIA, CMU and Microsoft Corporation
*
* Permission is hereby granted, free of charge, to any person obtaining a copy
* of this software and associated documentation files (the "Software"), to deal
* in the Software without restriction, including without limitation the rights
* to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
* copies of the Software, and to permit persons to whom the Software is
* furnished to do so, subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in all
* copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
* AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
* OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
* SOFTWARE.
*/
#ifndef __MerkleTree_H
#define __MerkleTree_H
#if defined(__cplusplus)
extern "C" {
#endif
#include "kremlin/internal/types.h"
#include "kremlin/lowstar_endianness.h"
#include <string.h>
#include "kremlin/internal/target.h"
static inline uint8_t FStar_UInt8_eq_mask(uint8_t a, uint8_t b);
typedef struct MerkleTree_Low_Datastructures_hash_vec_s
{
uint32_t sz;
uint32_t cap;
uint8_t **vs;
}
MerkleTree_Low_Datastructures_hash_vec;
typedef uint32_t hash_size_t;
typedef uint64_t offset_t;
typedef uint32_t index_t;
typedef struct MerkleTree_Low_path_s
{
uint32_t hash_size;
MerkleTree_Low_Datastructures_hash_vec hashes;
}
MerkleTree_Low_path;
typedef MerkleTree_Low_path path;
typedef MerkleTree_Low_path *path_p;
typedef const MerkleTree_Low_path *const_path_p;
typedef struct MerkleTree_Low_Datastructures_hash_vv_s
{
uint32_t sz;
uint32_t cap;
MerkleTree_Low_Datastructures_hash_vec *vs;
}
MerkleTree_Low_Datastructures_hash_vv;
typedef struct MerkleTree_Low_merkle_tree_s
{
uint32_t hash_size;
uint64_t offset;
uint32_t i;
uint32_t j;
MerkleTree_Low_Datastructures_hash_vv hs;
bool rhs_ok;
MerkleTree_Low_Datastructures_hash_vec rhs;
uint8_t *mroot;
void (*hash_fun)(uint8_t *x0, uint8_t *x1, uint8_t *x2);
}
MerkleTree_Low_merkle_tree;
typedef MerkleTree_Low_merkle_tree merkle_tree;
typedef MerkleTree_Low_merkle_tree *mt_p;
typedef const MerkleTree_Low_merkle_tree *const_mt_p;
/*
Constructor for hashes
*/
uint8_t *mt_init_hash(uint32_t hash_size);
/*
Destructor for hashes
*/
void mt_free_hash(uint8_t *h);
/*
Constructor for paths
*/
MerkleTree_Low_path *mt_init_path(uint32_t hash_size);
/*
Destructor for paths
*/
void mt_free_path(MerkleTree_Low_path *path1);
/*
Length of a path
@param[in] p Path
return The length of the path
*/
uint32_t mt_get_path_length(const MerkleTree_Low_path *path1);
/*
Insert hash into path
@param[in] p Path
@param[in] hash Hash to insert
*/
void mt_path_insert(MerkleTree_Low_path *path1, uint8_t *hash1);
/*
Get step on a path
@param[in] p Path
@param[in] i Path step index
return The hash at step i of p
*/
uint8_t *mt_get_path_step(const MerkleTree_Low_path *path1, uint32_t i);
/*
Precondition predicate for mt_get_path_step
*/
bool mt_get_path_step_pre(const MerkleTree_Low_path *path1, uint32_t i);
/*
Construction with custom hash functions
@param[in] hash_size Hash size (in bytes)
@param[in] i The initial hash
return The new Merkle tree
*/
MerkleTree_Low_merkle_tree
*mt_create_custom(
uint32_t hash_size,
uint8_t *i,
void (*hash_fun)(uint8_t *x0, uint8_t *x1, uint8_t *x2)
);
/*
Destruction
@param[in] mt The Merkle tree
*/
void mt_free(MerkleTree_Low_merkle_tree *mt);
/*
Insertion
@param[in] mt The Merkle tree
@param[in] v The tree does not take ownership of the hash, it makes a copy of its content.
Note: The content of the hash will be overwritten with an arbitrary value.
*/
void mt_insert(MerkleTree_Low_merkle_tree *mt, uint8_t *v);
/*
Precondition predicate for mt_insert
*/
bool mt_insert_pre(const MerkleTree_Low_merkle_tree *mt, uint8_t *v);
/*
Getting the Merkle root
@param[in] mt The Merkle tree
@param[out] root The Merkle root
*/
void mt_get_root(const MerkleTree_Low_merkle_tree *mt, uint8_t *root);
/*
Precondition predicate for mt_get_root
*/
bool mt_get_root_pre(const MerkleTree_Low_merkle_tree *mt, uint8_t *root);
/*
Getting a Merkle path
@param[in] mt The Merkle tree
@param[in] idx The index of the target hash
@param[out] path A resulting Merkle path that contains the leaf hash.
@param[out] root The Merkle root
return The number of elements in the tree
Notes:
- The resulting path contains pointers to hashes in the tree, not copies of
the hash values.
- idx must be within the currently held indices in the tree (past the
last flush index).
*/
uint32_t
mt_get_path(
const MerkleTree_Low_merkle_tree *mt,
uint64_t idx,
MerkleTree_Low_path *path1,
uint8_t *root
);
/*
Precondition predicate for mt_get_path
*/
bool
mt_get_path_pre(
const MerkleTree_Low_merkle_tree *mt,
uint64_t idx,
const MerkleTree_Low_path *path1,
uint8_t *root
);
/*
Flush the Merkle tree
@param[in] mt The Merkle tree
*/
void mt_flush(MerkleTree_Low_merkle_tree *mt);
/*
Precondition predicate for mt_flush
*/
bool mt_flush_pre(const MerkleTree_Low_merkle_tree *mt);
/*
Flush the Merkle tree up to a given index
@param[in] mt The Merkle tree
@param[in] idx The index up to which to flush the tree
*/
void mt_flush_to(MerkleTree_Low_merkle_tree *mt, uint64_t idx);
/*
Precondition predicate for mt_flush_to
*/
bool mt_flush_to_pre(const MerkleTree_Low_merkle_tree *mt, uint64_t idx);
/*
Retract the Merkle tree down to a given index
@param[in] mt The Merkle tree
@param[in] idx The index to retract the tree to
Note: The element and idx will remain in the tree.
*/
void mt_retract_to(MerkleTree_Low_merkle_tree *mt, uint64_t idx);
/*
Precondition predicate for mt_retract_to
*/
bool mt_retract_to_pre(const MerkleTree_Low_merkle_tree *mt, uint64_t idx);
/*
Client-side verification
@param[in] mt The Merkle tree
@param[in] tgt The index of the target hash
@param[in] max The maximum index + 1 of the tree when the path was generated
@param[in] path The Merkle path to verify
@param[in] root
return true if the verification succeeded, false otherwise
Note: max - tgt must be less than 2^32.
*/
bool
mt_verify(
const MerkleTree_Low_merkle_tree *mt,
uint64_t tgt,
uint64_t max,
const MerkleTree_Low_path *path1,
uint8_t *root
);
/*
Precondition predicate for mt_verify
*/
bool
mt_verify_pre(
const MerkleTree_Low_merkle_tree *mt,
uint64_t tgt,
uint64_t max,
const MerkleTree_Low_path *path1,
uint8_t *root
);
/*
Serialization size
@param[in] mt The Merkle tree
return the number of bytes required to serialize the tree
*/
uint64_t mt_serialize_size(const MerkleTree_Low_merkle_tree *mt);
/*
Merkle tree serialization
@param[in] mt The Merkle tree
@param[out] buf The buffer to serialize the tree into
@param[in] len Length of buf
return the number of bytes written
Note: buf must be a buffer of size mt_serialize_size(mt) or larger, but
smaller than 2^32 (larger buffers are currently not supported).
*/
uint64_t mt_serialize(const MerkleTree_Low_merkle_tree *mt, uint8_t *buf, uint64_t len);
/*
Merkle tree deserialization
@param[in] expected_hash_size Expected hash size to match hash_fun
@param[in] buf The buffer to deserialize the tree from
@param[in] len Length of buf
@param[in] hash_fun Hash function
return pointer to the new tree if successful, NULL otherwise
Note: buf must point to an allocated buffer.
*/
MerkleTree_Low_merkle_tree
*mt_deserialize(
const uint8_t *buf,
uint64_t len,
void (*hash_fun)(uint8_t *x0, uint8_t *x1, uint8_t *x2)
);
/*
Path serialization
@param[in] path The path
@param[out] buf The buffer to serialize the path into
@param[in] len Length of buf
return the number of bytes written
*/
uint64_t mt_serialize_path(const MerkleTree_Low_path *path1, uint8_t *buf, uint64_t len);
/*
Path deserialization
@param[in] buf The buffer to deserialize the path from
@param[in] len Length of buf
return pointer to the new path if successful, NULL otherwise
Note: buf must point to an allocated buffer.
*/
MerkleTree_Low_path *mt_deserialize_path(const uint8_t *buf, uint64_t len);
typedef uint32_t MerkleTree_Low_index_t;
extern uint32_t MerkleTree_Low_uint32_32_max;
extern uint64_t MerkleTree_Low_uint32_max;
extern uint64_t MerkleTree_Low_uint64_max;
extern uint64_t MerkleTree_Low_offset_range_limit;
typedef uint64_t MerkleTree_Low_offset_t;
extern uint32_t MerkleTree_Low_merkle_tree_size_lg;
bool MerkleTree_Low_uu___is_MT(MerkleTree_Low_merkle_tree projectee);
uint32_t MerkleTree_Low___proj__MT__item__hash_size(MerkleTree_Low_merkle_tree projectee);
uint64_t MerkleTree_Low___proj__MT__item__offset(MerkleTree_Low_merkle_tree projectee);
uint32_t MerkleTree_Low___proj__MT__item__i(MerkleTree_Low_merkle_tree projectee);
uint32_t MerkleTree_Low___proj__MT__item__j(MerkleTree_Low_merkle_tree projectee);
MerkleTree_Low_Datastructures_hash_vv
MerkleTree_Low___proj__MT__item__hs(MerkleTree_Low_merkle_tree projectee);
bool MerkleTree_Low___proj__MT__item__rhs_ok(MerkleTree_Low_merkle_tree projectee);
MerkleTree_Low_Datastructures_hash_vec
MerkleTree_Low___proj__MT__item__rhs(MerkleTree_Low_merkle_tree projectee);
uint8_t *MerkleTree_Low___proj__MT__item__mroot(MerkleTree_Low_merkle_tree projectee);
void
(*MerkleTree_Low___proj__MT__item__hash_fun(MerkleTree_Low_merkle_tree projectee))(
uint8_t *x0,
uint8_t *x1,
uint8_t *x2
);
typedef MerkleTree_Low_merkle_tree *MerkleTree_Low_mt_p;
typedef const MerkleTree_Low_merkle_tree *MerkleTree_Low_const_mt_p;
bool
MerkleTree_Low_merkle_tree_conditions(
uint64_t offset,
uint32_t i,
uint32_t j,
MerkleTree_Low_Datastructures_hash_vv hs,
bool rhs_ok,
MerkleTree_Low_Datastructures_hash_vec rhs,
uint8_t *mroot
);
uint32_t MerkleTree_Low_offset_of(uint32_t i);
void MerkleTree_Low_mt_free(MerkleTree_Low_merkle_tree *mt);
bool MerkleTree_Low_mt_insert_pre(const MerkleTree_Low_merkle_tree *mt, uint8_t *v);
void MerkleTree_Low_mt_insert(MerkleTree_Low_merkle_tree *mt, uint8_t *v);
MerkleTree_Low_merkle_tree
*MerkleTree_Low_mt_create_custom(
uint32_t hsz,
uint8_t *init,
void (*hash_fun)(uint8_t *x0, uint8_t *x1, uint8_t *x2)
);
bool MerkleTree_Low_uu___is_Path(MerkleTree_Low_path projectee);
uint32_t MerkleTree_Low___proj__Path__item__hash_size(MerkleTree_Low_path projectee);
MerkleTree_Low_Datastructures_hash_vec
MerkleTree_Low___proj__Path__item__hashes(MerkleTree_Low_path projectee);
typedef MerkleTree_Low_path *MerkleTree_Low_path_p;
typedef const MerkleTree_Low_path *MerkleTree_Low_const_path_p;
MerkleTree_Low_path *MerkleTree_Low_init_path(uint32_t hsz);
void MerkleTree_Low_clear_path(MerkleTree_Low_path *p);
void MerkleTree_Low_free_path(MerkleTree_Low_path *p);
bool MerkleTree_Low_mt_get_root_pre(const MerkleTree_Low_merkle_tree *mt, uint8_t *rt);
void MerkleTree_Low_mt_get_root(const MerkleTree_Low_merkle_tree *mt, uint8_t *rt);
void MerkleTree_Low_mt_path_insert(uint32_t hsz, MerkleTree_Low_path *p, uint8_t *hp);
uint32_t MerkleTree_Low_mt_get_path_length(const MerkleTree_Low_path *p);
bool MerkleTree_Low_mt_get_path_step_pre(const MerkleTree_Low_path *p, uint32_t i);
uint8_t *MerkleTree_Low_mt_get_path_step(const MerkleTree_Low_path *p, uint32_t i);
bool
MerkleTree_Low_mt_get_path_pre(
const MerkleTree_Low_merkle_tree *mt,
uint64_t idx,
const MerkleTree_Low_path *p,
uint8_t *root
);
uint32_t
MerkleTree_Low_mt_get_path(
const MerkleTree_Low_merkle_tree *mt,
uint64_t idx,
MerkleTree_Low_path *p,
uint8_t *root
);
bool MerkleTree_Low_mt_flush_to_pre(const MerkleTree_Low_merkle_tree *mt, uint64_t idx);
void MerkleTree_Low_mt_flush_to(MerkleTree_Low_merkle_tree *mt, uint64_t idx);
bool MerkleTree_Low_mt_flush_pre(const MerkleTree_Low_merkle_tree *mt);
void MerkleTree_Low_mt_flush(MerkleTree_Low_merkle_tree *mt);
bool MerkleTree_Low_mt_retract_to_pre(const MerkleTree_Low_merkle_tree *mt, uint64_t r);
void MerkleTree_Low_mt_retract_to(MerkleTree_Low_merkle_tree *mt, uint64_t r);
bool
MerkleTree_Low_mt_verify_pre(
const MerkleTree_Low_merkle_tree *mt,
uint64_t k,
uint64_t j,
const MerkleTree_Low_path *p,
uint8_t *rt
);
bool
MerkleTree_Low_mt_verify(
const MerkleTree_Low_merkle_tree *mt,
uint64_t k,
uint64_t j,
const MerkleTree_Low_path *p,
uint8_t *rt
);
typedef uint8_t MerkleTree_Low_Serialization_uint8_t;
typedef uint16_t MerkleTree_Low_Serialization_uint16_t;
typedef uint32_t MerkleTree_Low_Serialization_uint32_t;
typedef uint64_t MerkleTree_Low_Serialization_uint64_t;
typedef uint8_t *MerkleTree_Low_Serialization_uint8_p;
typedef const uint8_t *MerkleTree_Low_Serialization_const_uint8_p;
uint64_t MerkleTree_Low_Serialization_mt_serialize_size(const MerkleTree_Low_merkle_tree *mt);
uint64_t
MerkleTree_Low_Serialization_mt_serialize(
const MerkleTree_Low_merkle_tree *mt,
uint8_t *output,
uint64_t sz
);
MerkleTree_Low_merkle_tree
*MerkleTree_Low_Serialization_mt_deserialize(
const uint8_t *input,
uint64_t sz,
void (*hash_fun)(uint8_t *x0, uint8_t *x1, uint8_t *x2)
);
uint64_t
MerkleTree_Low_Serialization_mt_serialize_path(
const MerkleTree_Low_path *p,
uint8_t *output,
uint64_t sz
);
MerkleTree_Low_path
*MerkleTree_Low_Serialization_mt_deserialize_path(const uint8_t *input, uint64_t sz);
uint8_t *MerkleTree_Low_Hashfunctions_init_hash(uint32_t hsz);
void MerkleTree_Low_Hashfunctions_free_hash(uint8_t *h);
#if defined(__cplusplus)
}
#endif
#define __MerkleTree_H_DEFINED
#endif
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...