Bitcoin jet costs

C/Makefile

@@ -1,5 +1,5 @@
 CORE_OBJS := bitstream.o dag.o deserialize.o eval.o frame.o jets.o jets-secp256k1.o rsort.o sha256.o type.o typeInference.o
-BITCOIN_OBJS := bitcoin/env.o bitcoin/ops.o bitcoin/bitcoinJets.o bitcoin/txEnv.o
+BITCOIN_OBJS := bitcoin/env.o bitcoin/ops.o bitcoin/bitcoinJets.o bitcoin/primitive.o bitcoin/txEnv.o
 ELEMENTS_OBJS := elements/env.o elements/exec.o elements/ops.o elements/elementsJets.o elements/primitive.o elements/cmr.o elements/txEnv.o
 TEST_OBJS := test.o ctx8Pruned.o ctx8Unpruned.o hashBlock.o regression4.o schnorr0.o schnorr6.o typeSkipTest.o elements/checkSigHashAllTx1.o
 

C/bitcoin/decodeBitcoinJets.inc

@@ -0,0 +1,87 @@
+/* This file has been automatically generated. */
+
+{
+  int32_t code;
+  code = simplicity_decodeUptoMaxInt(stream);
+  if (code < 0) return (simplicity_err)code;
+  switch (code) {
+    case 1:
+      code = simplicity_decodeUptoMaxInt(stream);
+      if (code < 0) return (simplicity_err)code;
+      switch (code) {
+        case 1: *result = SIG_ALL_HASH; return SIMPLICITY_NO_ERROR;
+        case 2: *result = TX_HASH; return SIMPLICITY_NO_ERROR;
+        case 3: *result = TAP_ENV_HASH; return SIMPLICITY_NO_ERROR;
+        case 4: *result = OUTPUTS_HASH; return SIMPLICITY_NO_ERROR;
+        case 5: *result = INPUTS_HASH; return SIMPLICITY_NO_ERROR;
+        case 6: *result = INPUT_UTXOS_HASH; return SIMPLICITY_NO_ERROR;
+        case 7: *result = OUTPUT_HASH; return SIMPLICITY_NO_ERROR;
+        case 8: *result = OUTPUT_VALUES_HASH; return SIMPLICITY_NO_ERROR;
+        case 9: *result = OUTPUT_SCRIPTS_HASH; return SIMPLICITY_NO_ERROR;
+        case 10: *result = INPUT_HASH; return SIMPLICITY_NO_ERROR;
+        case 11: *result = INPUT_OUTPOINTS_HASH; return SIMPLICITY_NO_ERROR;
+        case 12: *result = INPUT_SEQUENCES_HASH; return SIMPLICITY_NO_ERROR;
+        case 13: *result = INPUT_ANNEXES_HASH; return SIMPLICITY_NO_ERROR;
+        case 14: *result = INPUT_SCRIPT_SIGS_HASH; return SIMPLICITY_NO_ERROR;
+        case 15: *result = INPUT_UTXO_HASH; return SIMPLICITY_NO_ERROR;
+        case 16: *result = INPUT_VALUES_HASH; return SIMPLICITY_NO_ERROR;
+        case 17: *result = INPUT_SCRIPTS_HASH; return SIMPLICITY_NO_ERROR;
+        case 18: *result = TAPLEAF_HASH; return SIMPLICITY_NO_ERROR;
+        case 19: *result = TAPPATH_HASH; return SIMPLICITY_NO_ERROR;
+        case 20: *result = OUTPOINT_HASH; return SIMPLICITY_NO_ERROR;
+        case 21: *result = ANNEX_HASH; return SIMPLICITY_NO_ERROR;
+        case 22: *result = BUILD_TAPLEAF_SIMPLICITY; return SIMPLICITY_NO_ERROR;
+        case 23: *result = BUILD_TAPBRANCH; return SIMPLICITY_NO_ERROR;
+        case 24: *result = BUILD_TAPTWEAK; return SIMPLICITY_NO_ERROR;
+      }
+      break;
+    case 2:
+      code = simplicity_decodeUptoMaxInt(stream);
+      if (code < 0) return (simplicity_err)code;
+      switch (code) {
+        case 1: *result = CHECK_LOCK_HEIGHT; return SIMPLICITY_NO_ERROR;
+        case 2: *result = CHECK_LOCK_TIME; return SIMPLICITY_NO_ERROR;
+        case 3: *result = CHECK_LOCK_DISTANCE; return SIMPLICITY_NO_ERROR;
+        case 4: *result = CHECK_LOCK_DURATION; return SIMPLICITY_NO_ERROR;
+        case 5: *result = TX_LOCK_HEIGHT; return SIMPLICITY_NO_ERROR;
+        case 6: *result = TX_LOCK_TIME; return SIMPLICITY_NO_ERROR;
+        case 7: *result = TX_LOCK_DISTANCE; return SIMPLICITY_NO_ERROR;
+        case 8: *result = TX_LOCK_DURATION; return SIMPLICITY_NO_ERROR;
+        case 9: *result = TX_IS_FINAL; return SIMPLICITY_NO_ERROR;
+      }
+      break;
+    case 3:
+      code = simplicity_decodeUptoMaxInt(stream);
+      if (code < 0) return (simplicity_err)code;
+      switch (code) {
+        case 1: *result = SCRIPT_CMR; return SIMPLICITY_NO_ERROR;
+        case 2: *result = INTERNAL_KEY; return SIMPLICITY_NO_ERROR;
+        case 3: *result = CURRENT_INDEX; return SIMPLICITY_NO_ERROR;
+        case 4: *result = NUM_INPUTS; return SIMPLICITY_NO_ERROR;
+        case 5: *result = NUM_OUTPUTS; return SIMPLICITY_NO_ERROR;
+        case 6: *result = LOCK_TIME; return SIMPLICITY_NO_ERROR;
+        case 7: *result = FEE; return SIMPLICITY_NO_ERROR;
+        case 8: *result = OUTPUT_VALUE; return SIMPLICITY_NO_ERROR;
+        case 9: *result = OUTPUT_SCRIPT_HASH; return SIMPLICITY_NO_ERROR;
+        case 10: *result = TOTAL_OUTPUT_VALUE; return SIMPLICITY_NO_ERROR;
+        case 11: *result = CURRENT_PREV_OUTPOINT; return SIMPLICITY_NO_ERROR;
+        case 12: *result = CURRENT_VALUE; return SIMPLICITY_NO_ERROR;
+        case 13: *result = CURRENT_SCRIPT_HASH; return SIMPLICITY_NO_ERROR;
+        case 14: *result = CURRENT_SEQUENCE; return SIMPLICITY_NO_ERROR;
+        case 15: *result = CURRENT_ANNEX_HASH; return SIMPLICITY_NO_ERROR;
+        case 16: *result = CURRENT_SCRIPT_SIG_HASH; return SIMPLICITY_NO_ERROR;
+        case 17: *result = INPUT_PREV_OUTPOINT; return SIMPLICITY_NO_ERROR;
+        case 18: *result = INPUT_VALUE; return SIMPLICITY_NO_ERROR;
+        case 19: *result = INPUT_SCRIPT_HASH; return SIMPLICITY_NO_ERROR;
+        case 20: *result = INPUT_SEQUENCE; return SIMPLICITY_NO_ERROR;
+        case 21: *result = INPUT_ANNEX_HASH; return SIMPLICITY_NO_ERROR;
+        case 22: *result = INPUT_SCRIPT_SIG_HASH; return SIMPLICITY_NO_ERROR;
+        case 23: *result = TOTAL_INPUT_VALUE; return SIMPLICITY_NO_ERROR;
+        case 24: *result = TAPLEAF_VERSION; return SIMPLICITY_NO_ERROR;
+        case 25: *result = TAPPATH; return SIMPLICITY_NO_ERROR;
+        case 26: *result = VERSION; return SIMPLICITY_NO_ERROR;
+        case 27: *result = TRANSACTION_ID; return SIMPLICITY_NO_ERROR;
+      }
+      break;
+  }
+}

C/bitcoin/primitive.c

@@ -0,0 +1,107 @@
+/* This module implements the 'primitive.h' interface for the Bitcoin application of Simplicity.
+ */
+#include "primitive.h"
+
+#include "bitcoinJets.h"
+#include "../limitations.h"
+#include "../simplicity_alloc.h"
+#include "../simplicity_assert.h"
+
+/* An enumeration of all the types we need to construct to specify the input and output types of all jets created by 'decodeJet'. */
+enum TypeNamesForJets {
+#include "primitiveEnumTy.inc"
+  NumberOfTypeNames
+};
+
+/* Allocate a fresh set of unification variables bound to at least all the types necessary
+ * for all the jets that can be created by 'decodeJet', and also the type 'TWO^256',
+ * and also allocate space for 'extra_var_len' many unification variables.
+ * Return the number of non-trivial bindings created.
+ *
+ * However, if malloc fails, then return 0.
+ *
+ * Precondition: NULL != bound_var;
+ *               NULL != word256_ix;
+ *               NULL != extra_var_start;
+ *               extra_var_len <= 6*DAG_LEN_MAX;
+ *
+ * Postcondition: Either '*bound_var == NULL' and the function returns 0
+ *                or 'unification_var (*bound_var)[*extra_var_start + extra_var_len]' is an array of unification variables
+ *                   such that for any 'jet : A |- B' there is some 'i < *extra_var_start' and 'j < *extra_var_start' such that
+ *                      '(*bound_var)[i]' is bound to 'A' and '(*bound_var)[j]' is bound to 'B'
+ *                   and, '*word256_ix < *extra_var_start' and '(*bound_var)[*word256_ix]' is bound the type 'TWO^256'
+ */
+size_t simplicity_bitcoin_mallocBoundVars(unification_var** bound_var, size_t* word256_ix, size_t* extra_var_start, size_t extra_var_len) {
+  static_assert(1 <= NumberOfTypeNames, "Missing TypeNamesForJets.");
+  static_assert(NumberOfTypeNames <= NUMBER_OF_TYPENAMES_MAX, "Too many TypeNamesForJets.");
+  static_assert(DAG_LEN_MAX <= (SIZE_MAX - NumberOfTypeNames) / 6, "NumberOfTypeNames + 6*DAG_LEN_MAX doesn't fit in size_t");
+  static_assert(NumberOfTypeNames + 6*DAG_LEN_MAX <= SIZE_MAX/sizeof(unification_var) , "bound_var array too large");
+  static_assert(NumberOfTypeNames + 6*DAG_LEN_MAX - 1 <= UINT32_MAX, "bound_var array index doesn't fit in uint32_t");
+  simplicity_assert(extra_var_len <= 6*DAG_LEN_MAX);
+  *bound_var = simplicity_malloc((NumberOfTypeNames + extra_var_len) * sizeof(unification_var));
+  if (!(*bound_var)) return 0;
+#include "primitiveInitTy.inc"
+  *word256_ix = ty_w256;
+  *extra_var_start = NumberOfTypeNames;
+
+  /* 'ty_u' is a trivial binding, so we made 'NumberOfTypeNames - 1' non-trivial bindings. */
+  return NumberOfTypeNames - 1;
+};
+
+/* An enumeration of the names of Bitcoin specific jets and primitives. */
+typedef enum jetName
+{
+#include "primitiveEnumJet.inc"
+  NUMBER_OF_JET_NAMES
+} jetName;
+
+/* Decode an Bitcoin specific jet name from 'stream' into 'result'.
+ * All jets begin with a bit prefix of '1' which needs to have already been consumed from the 'stream'.
+ * Returns 'SIMPLICITY_ERR_DATA_OUT_OF_RANGE' if the stream's prefix doesn't match any valid code for a jet.
+ * Returns 'SIMPLICITY_ERR_BITSTRING_EOF' if not enough bits are available in the 'stream'.
+ * In the above error cases, 'result' may be modified.
+ * Returns 'SIMPLICITY_NO_ERROR' if successful.
+ *
+ * Precondition: NULL != result
+ *               NULL != stream
+ */
+static simplicity_err decodePrimitive(jetName* result, bitstream* stream) {
+  int32_t bit = read1Bit(stream);
+  if (bit < 0) return (simplicity_err)bit;
+  if (!bit) {
+    /* Core jets */
+#include "../decodeCoreJets.inc"
+    return SIMPLICITY_ERR_DATA_OUT_OF_RANGE;
+  } else {
+    /* Bitcoin jets */
+#include "decodeBitcoinJets.inc"
+    return SIMPLICITY_ERR_DATA_OUT_OF_RANGE;
+  }
+}
+
+/* Return a copy of the Simplicity node corresponding to the given Bitcoin specific jet 'name'. */
+static dag_node jetNode(jetName name) {
+  static const dag_node jet_node[] = {
+    #include "primitiveJetNode.inc"
+  };
+
+  return jet_node[name];
+}
+
+/* Decode a Bitcoin specific jet from 'stream' into 'node'.
+ * All jets begin with a bit prefix of '1' which needs to have already been consumed from the 'stream'.
+ * Returns 'SIMPLICITY_ERR_DATA_OUT_OF_RANGE' if the stream's prefix doesn't match any valid code for a jet.
+ * Returns 'SIMPLICITY_ERR_BITSTRING_EOF' if not enough bits are available in the 'stream'.
+ * In the above error cases, 'dag' may be modified.
+ * Returns 'SIMPLICITY_NO_ERR' if successful.
+ *
+ * Precondition: NULL != node
+ *               NULL != stream
+ */
+simplicity_err simplicity_bitcoin_decodeJet(dag_node* node, bitstream* stream) {
+  jetName name;
+  simplicity_err error = decodePrimitive(&name, stream);
+  if (!IS_OK(error)) return error;
+  *node = jetNode(name);
+  return SIMPLICITY_NO_ERROR;
+}

C/bitcoin/primitive.h

@@ -0,0 +1,41 @@
+/* Implements the primitive.h interface for the Bitcoin Simplicity application.
+ */
+#ifndef SIMPLICITY_BITCOIN_PRIMITIVE_H
+#define SIMPLICITY_BITCOIN_PRIMITIVE_H
+
+#include "../bitstream.h"
+#include "../typeInference.h"
+
+/* Allocate a fresh set of unification variables bound to at least all the types necessary
+ * for all the jets that can be created by 'decodeJet', and also the type 'TWO^256',
+ * and also allocate space for 'extra_var_len' many unification variables.
+ * Return the number of non-trivial bindings created.
+ *
+ * However, if malloc fails, then return 0.
+ *
+ * Precondition: NULL != bound_var;
+ *               NULL != word256_ix;
+ *               NULL != extra_var_start;
+ *               extra_var_len <= 6*DAG_LEN_MAX;
+ *
+ * Postcondition: Either '*bound_var == NULL' and the function returns 0
+ *                or 'unification_var (*bound_var)[*extra_var_start + extra_var_len]' is an array of unification variables
+ *                   such that for any 'jet : A |- B' there is some 'i < *extra_var_start' and 'j < *extra_var_start' such that
+ *                      '(*bound_var)[i]' is bound to 'A' and '(*bound_var)[j]' is bound to 'B'
+ *                   and, '*word256_ix < *extra_var_start' and '(*bound_var)[*word256_ix]' is bound the type 'TWO^256'
+ */
+size_t simplicity_bitcoin_mallocBoundVars(unification_var** bound_var, size_t* word256_ix, size_t* extra_var_start, size_t extra_var_len);
+
+/* Decode a Bitcoin specific jet from 'stream' into 'node'.
+ * All jets begin with a bit prefix of '1' which needs to have already been consumed from the 'stream'.
+ * Returns 'SIMPLICITY_ERR_DATA_OUT_OF_RANGE' if the stream's prefix doesn't match any valid code for a jet.
+ * Returns 'SIMPLICITY_ERR_BITSTRING_EOF' if not enough bits are available in the 'stream'.
+ * In the above error cases, 'dag' may be modified.
+ * Returns 'SIMPLICITY_NO_ERROR' if successful.
+ *
+ * Precondition: NULL != node
+ *               NULL != stream
+ */
+simplicity_err simplicity_bitcoin_decodeJet(dag_node* node, bitstream* stream);
+
+#endif