|
| 1 | +/* This module implements the 'primitive.h' interface for the Bitcoin application of Simplicity. |
| 2 | + */ |
| 3 | +#include "primitive.h" |
| 4 | + |
| 5 | +#include "bitcoinJets.h" |
| 6 | +#include "../limitations.h" |
| 7 | +#include "../simplicity_alloc.h" |
| 8 | +#include "../simplicity_assert.h" |
| 9 | + |
| 10 | +/* An enumeration of all the types we need to construct to specify the input and output types of all jets created by 'decodeJet'. */ |
| 11 | +enum TypeNamesForJets { |
| 12 | +#include "primitiveEnumTy.inc" |
| 13 | + NumberOfTypeNames |
| 14 | +}; |
| 15 | + |
| 16 | +/* Allocate a fresh set of unification variables bound to at least all the types necessary |
| 17 | + * for all the jets that can be created by 'decodeJet', and also the type 'TWO^256', |
| 18 | + * and also allocate space for 'extra_var_len' many unification variables. |
| 19 | + * Return the number of non-trivial bindings created. |
| 20 | + * |
| 21 | + * However, if malloc fails, then return 0. |
| 22 | + * |
| 23 | + * Precondition: NULL != bound_var; |
| 24 | + * NULL != word256_ix; |
| 25 | + * NULL != extra_var_start; |
| 26 | + * extra_var_len <= 6*DAG_LEN_MAX; |
| 27 | + * |
| 28 | + * Postcondition: Either '*bound_var == NULL' and the function returns 0 |
| 29 | + * or 'unification_var (*bound_var)[*extra_var_start + extra_var_len]' is an array of unification variables |
| 30 | + * such that for any 'jet : A |- B' there is some 'i < *extra_var_start' and 'j < *extra_var_start' such that |
| 31 | + * '(*bound_var)[i]' is bound to 'A' and '(*bound_var)[j]' is bound to 'B' |
| 32 | + * and, '*word256_ix < *extra_var_start' and '(*bound_var)[*word256_ix]' is bound the type 'TWO^256' |
| 33 | + */ |
| 34 | +size_t simplicity_bitcoin_mallocBoundVars(unification_var** bound_var, size_t* word256_ix, size_t* extra_var_start, size_t extra_var_len) { |
| 35 | + static_assert(1 <= NumberOfTypeNames, "Missing TypeNamesForJets."); |
| 36 | + static_assert(NumberOfTypeNames <= NUMBER_OF_TYPENAMES_MAX, "Too many TypeNamesForJets."); |
| 37 | + static_assert(DAG_LEN_MAX <= (SIZE_MAX - NumberOfTypeNames) / 6, "NumberOfTypeNames + 6*DAG_LEN_MAX doesn't fit in size_t"); |
| 38 | + static_assert(NumberOfTypeNames + 6*DAG_LEN_MAX <= SIZE_MAX/sizeof(unification_var) , "bound_var array too large"); |
| 39 | + static_assert(NumberOfTypeNames + 6*DAG_LEN_MAX - 1 <= UINT32_MAX, "bound_var array index doesn't fit in uint32_t"); |
| 40 | + simplicity_assert(extra_var_len <= 6*DAG_LEN_MAX); |
| 41 | + *bound_var = simplicity_malloc((NumberOfTypeNames + extra_var_len) * sizeof(unification_var)); |
| 42 | + if (!(*bound_var)) return 0; |
| 43 | +#include "primitiveInitTy.inc" |
| 44 | + *word256_ix = ty_w256; |
| 45 | + *extra_var_start = NumberOfTypeNames; |
| 46 | + |
| 47 | + /* 'ty_u' is a trivial binding, so we made 'NumberOfTypeNames - 1' non-trivial bindings. */ |
| 48 | + return NumberOfTypeNames - 1; |
| 49 | +}; |
| 50 | + |
| 51 | +/* An enumeration of the names of Bitcoin specific jets and primitives. */ |
| 52 | +typedef enum jetName |
| 53 | +{ |
| 54 | +#include "primitiveEnumJet.inc" |
| 55 | + NUMBER_OF_JET_NAMES |
| 56 | +} jetName; |
| 57 | + |
| 58 | +/* Decode an Bitcoin specific jet name from 'stream' into 'result'. |
| 59 | + * All jets begin with a bit prefix of '1' which needs to have already been consumed from the 'stream'. |
| 60 | + * Returns 'SIMPLICITY_ERR_DATA_OUT_OF_RANGE' if the stream's prefix doesn't match any valid code for a jet. |
| 61 | + * Returns 'SIMPLICITY_ERR_BITSTRING_EOF' if not enough bits are available in the 'stream'. |
| 62 | + * In the above error cases, 'result' may be modified. |
| 63 | + * Returns 'SIMPLICITY_NO_ERROR' if successful. |
| 64 | + * |
| 65 | + * Precondition: NULL != result |
| 66 | + * NULL != stream |
| 67 | + */ |
| 68 | +static simplicity_err decodePrimitive(jetName* result, bitstream* stream) { |
| 69 | + int32_t bit = read1Bit(stream); |
| 70 | + if (bit < 0) return (simplicity_err)bit; |
| 71 | + if (!bit) { |
| 72 | + /* Core jets */ |
| 73 | +#include "../decodeCoreJets.inc" |
| 74 | + return SIMPLICITY_ERR_DATA_OUT_OF_RANGE; |
| 75 | + } else { |
| 76 | + /* Bitcoin jets */ |
| 77 | +#include "decodeBitcoinJets.inc" |
| 78 | + return SIMPLICITY_ERR_DATA_OUT_OF_RANGE; |
| 79 | + } |
| 80 | +} |
| 81 | + |
| 82 | +/* Return a copy of the Simplicity node corresponding to the given Bitcoin specific jet 'name'. */ |
| 83 | +static dag_node jetNode(jetName name) { |
| 84 | + static const dag_node jet_node[] = { |
| 85 | + #include "primitiveJetNode.inc" |
| 86 | + }; |
| 87 | + |
| 88 | + return jet_node[name]; |
| 89 | +} |
| 90 | + |
| 91 | +/* Decode a Bitcoin specific jet from 'stream' into 'node'. |
| 92 | + * All jets begin with a bit prefix of '1' which needs to have already been consumed from the 'stream'. |
| 93 | + * Returns 'SIMPLICITY_ERR_DATA_OUT_OF_RANGE' if the stream's prefix doesn't match any valid code for a jet. |
| 94 | + * Returns 'SIMPLICITY_ERR_BITSTRING_EOF' if not enough bits are available in the 'stream'. |
| 95 | + * In the above error cases, 'dag' may be modified. |
| 96 | + * Returns 'SIMPLICITY_NO_ERR' if successful. |
| 97 | + * |
| 98 | + * Precondition: NULL != node |
| 99 | + * NULL != stream |
| 100 | + */ |
| 101 | +simplicity_err simplicity_bitcoin_decodeJet(dag_node* node, bitstream* stream) { |
| 102 | + jetName name; |
| 103 | + simplicity_err error = decodePrimitive(&name, stream); |
| 104 | + if (!IS_OK(error)) return error; |
| 105 | + *node = jetNode(name); |
| 106 | + return SIMPLICITY_NO_ERROR; |
| 107 | +} |
0 commit comments