Timelock Jets

C/jets.c

@@ -79,3 +79,25 @@ bool sha_256_block(frameItem* dst, frameItem src, const txEnv* env) {
   write32s(dst, h, 8);
   return true;
 }
+
+/* parse_sequence : TWO^32 |- TWO^32 + TWO^32 */
+bool parse_lock(frameItem* dst, frameItem src, const txEnv* env) {
+  (void) env; // env is unused;
+  uint_fast32_t nLockTime = read32(&src);
+  writeBit(dst, 500000000U <= nLockTime);
+  write32(dst, nLockTime);
+  return true;
+}
+
+/* parse_sequence : TWO^32 |- S (TWO^16 + TWO^16) */
+bool parse_sequence(frameItem* dst, frameItem src, const txEnv* env) {
+  (void) env; // env is unused;
+  uint_fast32_t nSequence = read32(&src);
+  if (writeBit(dst, nSequence < ((uint_fast32_t)1 << 31))) {
+    writeBit(dst, nSequence & ((uint_fast32_t)1 << 22));
+    write16(dst, nSequence & 0xffff);
+  } else {
+    skipBits(dst, 17);
+  }
+  return true;
+}

C/jets.h

@@ -70,4 +70,7 @@ bool decompress(frameItem* dst, frameItem src, const txEnv* env);
 bool point_verify_1(frameItem* dst, frameItem src, const txEnv* env);
 bool bip_0340_verify(frameItem* dst, frameItem src, const txEnv* env);
 
+bool parse_lock(frameItem* dst, frameItem src, const txEnv* env);
+bool parse_sequence(frameItem* dst, frameItem src, const txEnv* env);
+
 #endif

C/primitive/elements/env.c

@@ -403,12 +403,22 @@ extern transaction* elements_simplicity_mallocTransaction(const rawTransaction*
                      , .numOutputs = rawTx->numOutputs
                      , .version = rawTx->version
                      , .lockTime = rawTx->lockTime
+                     , .isFinal = true
                      };
 
   {
     sha256_context ctx = sha256_init(tx->inputsHash.s);
     for (uint_fast32_t i = 0; i < tx->numInputs; ++i) {
       copyInput(&input[i], &rawTx->input[i]);
+      if (input[i].sequence < 0xffffffff) { tx->isFinal = false; }
+      if (input[i].sequence < 0x80000000) {
+         const uint_fast16_t maskedSequence = input[i].sequence & 0xffff;
+         if (input[i].sequence & ((uint_fast32_t)1 << 22)) {
+            if (tx->lockDuration < maskedSequence) tx->lockDuration = maskedSequence;
+         } else {
+            if (tx->lockDistance < maskedSequence) tx->lockDistance = maskedSequence;
+         }
+      }
       sha256_outpoint(&ctx, &input[i].prevOutpoint);
       sha256_u32le(&ctx, input[i].sequence);
       sha256_issuance(&ctx, &input[i].issuance);

C/primitive/elements/jets.c

@@ -139,6 +139,22 @@ static void issuanceTokenAmt(frameItem* dst, const assetIssuance* issuance) {
   }
 }
 
+static uint_fast32_t lockHeight(const transaction* tx) {
+  return !tx->isFinal && tx->lockTime < 500000000U ? tx->lockTime : 0;
+}
+
+static uint_fast32_t lockTime(const transaction* tx) {
+  return !tx->isFinal && 500000000U <= tx->lockTime ? tx->lockTime : 0;
+}
+
+static uint_fast16_t lockDistance(const transaction* tx) {
+  return 2 <= tx->version ? tx->lockDistance : 0;
+}
+
+static uint_fast16_t lockDuration(const transaction* tx) {
+  return 2 <= tx->version ? (uint_fast32_t)tx->lockDuration : 0;
+}
+
 /* version : ONE |- TWO^32 */
 bool version(frameItem* dst, frameItem src, const txEnv* env) {
   (void) src; // src is unused;
@@ -595,3 +611,66 @@ bool num_outputs(frameItem* dst, frameItem src, const txEnv* env) {
   write32(dst, env->tx->numOutputs);
   return true;
 }
+
+/* tx_is_final : ONE |- TWO */
+bool tx_is_final(frameItem* dst, frameItem src, const txEnv* env) {
+  (void) src; // src is unused;
+  writeBit(dst, env->tx->isFinal);
+  return true;
+}
+
+/* tx_lock_height : ONE |- TWO^32 */
+bool tx_lock_height(frameItem* dst, frameItem src, const txEnv* env) {
+  (void) src; // src is unused;
+  write32(dst, lockHeight(env->tx));
+  return true;
+}
+
+/* tx_lock_time : ONE |- TWO^32 */
+bool tx_lock_time(frameItem* dst, frameItem src, const txEnv* env) {
+  (void) src; // src is unused;
+  write32(dst, lockTime(env->tx));
+  return true;
+}
+
+/* tx_lock_distance : ONE |- TWO^16 */
+bool tx_lock_distance(frameItem* dst, frameItem src, const txEnv* env) {
+  (void) src; // src is unused;
+  write16(dst, lockDistance(env->tx));
+  return true;
+}
+
+/* tx_lock_duration : ONE |- TWO^16 */
+bool tx_lock_duration(frameItem* dst, frameItem src, const txEnv* env) {
+  (void) src; // src is unused;
+  write16(dst, lockDuration(env->tx));
+  return true;
+}
+
+/* check_lock_height : TWO^32 |- ONE */
+bool check_lock_height(frameItem* dst, frameItem src, const txEnv* env) {
+  (void) dst; // dst is unused;
+  uint_fast32_t x = read32(&src);
+  return x <= lockHeight(env->tx);
+}
+
+/* check_lock_time : TWO^32 |- ONE */
+bool check_lock_time(frameItem* dst, frameItem src, const txEnv* env) {
+  (void) dst; // dst is unused;
+  uint_fast32_t x = read32(&src);
+  return x <= lockTime(env->tx);
+}
+
+/* check_lock_distance : TWO^16 |- ONE */
+bool check_lock_distance(frameItem* dst, frameItem src, const txEnv* env) {
+  (void) dst; // dst is unused;
+  uint_fast16_t x = read16(&src);
+  return x <= lockDistance(env->tx);
+}
+
+/* check_lock_duration : TWO^16 |- ONE */
+bool check_lock_duration(frameItem* dst, frameItem src, const txEnv* env) {
+  (void) dst; // dst is unused;
+  uint_fast16_t x = read16(&src);
+  return x <= lockDuration(env->tx);
+}

C/primitive/elements/jets.h

@@ -55,4 +55,15 @@ bool num_outputs(frameItem* dst, frameItem src, const txEnv* env);
 /* :TODO: Not yet implemented. */
 #define fee NULL
 
+/* Jets for the Elements application of Simplicity. */
+bool tx_is_final(frameItem* dst, frameItem src, const txEnv* env);
+bool tx_lock_height(frameItem* dst, frameItem src, const txEnv* env);
+bool tx_lock_time(frameItem* dst, frameItem src, const txEnv* env);
+bool tx_lock_distance(frameItem* dst, frameItem src, const txEnv* env);
+bool tx_lock_duration(frameItem* dst, frameItem src, const txEnv* env);
+bool check_lock_height(frameItem* dst, frameItem src, const txEnv* env);
+bool check_lock_time(frameItem* dst, frameItem src, const txEnv* env);
+bool check_lock_distance(frameItem* dst, frameItem src, const txEnv* env);
+bool check_lock_duration(frameItem* dst, frameItem src, const txEnv* env);
+
 #endif

C/primitive/elements/primitive.c

@@ -261,11 +261,37 @@ static int32_t decodePrimitive(jetName* result, bitstream* stream) {
          case 1: *result = BIP_0340_VERIFY; return 0;
         }
         break;
+       case 7: /* Bitcoin jets chapter */
+        code = decodeUptoMaxInt(stream);
+        if (code < 0) return code;
+        switch (code) {
+         case 1: *result = PARSE_LOCK; return 0;
+         case 2: *result = PARSE_SEQUENCE; return 0;
+        }
+        break;
       }
       return SIMPLICITY_ERR_DATA_OUT_OF_RANGE;
-
     } else {
-      /* Elements specific jets go here */
+      /* Elements jets */
+      int32_t code = decodeUptoMaxInt(stream);
+      if (code < 0) return code;
+      switch (code) {
+       case 2: /* Timelock jets chapter */
+        code = decodeUptoMaxInt(stream);
+        if (code < 0) return code;
+        switch (code) {
+         case 1: *result = CHECK_LOCK_HEIGHT; return 0;
+         case 2: *result = CHECK_LOCK_TIME; return 0;
+         case 3: *result = CHECK_LOCK_DISTANCE; return 0;
+         case 4: *result = CHECK_LOCK_DURATION; return 0;
+         case 5: *result = TX_LOCK_HEIGHT; return 0;
+         case 6: *result = TX_LOCK_TIME; return 0;
+         case 7: *result = TX_LOCK_DISTANCE; return 0;
+         case 8: *result = TX_LOCK_DURATION; return 0;
+         case 9: *result = TX_IS_FINAL; return 0;
+        }
+        break;
+      }
       return SIMPLICITY_ERR_DATA_OUT_OF_RANGE;
     }
   }

C/primitive/elements/primitive.h

@@ -193,6 +193,12 @@ typedef struct transaction {
   uint_fast32_t numOutputs;
   uint_fast32_t version;
   uint_fast32_t lockTime;
+  /* lockDuration and lockDistance values are set even when the version is 0 or 1.
+   * This is similar to lockTime whose value is also set, even when the transaction is final.
+   */
+  uint_fast16_t lockDistance;
+  uint_fast16_t lockDuration; /* Units of 512 seconds */
+  bool isFinal;
 } transaction;
 
 /* A structure representing taproot spending data from an Elements transaction.

C/primitive/elements/primitiveEnumJet.inc

@@ -1,6 +1,9 @@
 /* This file has been automatically generated. */
+PARSE_SEQUENCE,
+CHECK_LOCK_HEIGHT,
 SCALAR_MULTIPLY,
 MULTIPLY_32,
+CHECK_LOCK_DURATION,
 GEJ_INFINITY,
 SCALAR_IS_ZERO,
 FULL_ADD_32,
@@ -13,8 +16,10 @@ SCALAR_ADD,
 SCALAR_NEGATE,
 FULL_SUBTRACT_32,
 GEJ_NEGATE,
+CHECK_LOCK_DISTANCE,
 GEJ_ADD,
 GEJ_DOUBLE,
+TX_LOCK_DURATION,
 FE_NEGATE,
 FE_SQUARE,
 SCALAR_NORMALIZE,
@@ -29,10 +34,14 @@ FE_MULTIPLY,
 GEJ_NORMALIZE,
 FE_INVERT,
 FE_NORMALIZE,
+CHECK_LOCK_TIME,
 FE_ADD,
 SCALAR_INVERT,
 POINT_VERIFY_1,
+TX_LOCK_DISTANCE,
 GEJ_Y_IS_ODD,
+TX_LOCK_TIME,
+PARSE_LOCK,
 SCALAR_SQUARE,
 GE_IS_ON_CURVE,
 GEJ_GE_ADD,
@@ -44,7 +53,9 @@ LINEAR_VERIFY_1,
 SCALAR_MULTIPLY_LAMBDA,
 SUBTRACT_32,
 FE_SQUARE_ROOT,
+TX_LOCK_HEIGHT,
 GEJ_RESCALE,
+TX_IS_FINAL,
 VERSION,
 LOCK_TIME,
 INPUT_IS_PEGIN,

C/primitive/elements/primitiveEnumTy.inc

@@ -19,11 +19,14 @@ ty_mmw256,
 ty_mmspbw256w64,
 ty_mmspbw256w256,
 ty_mmspw2w256sbw4,
+ty_msw16w16,
 ty_mspbw256w64,
 ty_mspbw256w256,
 ty_mspw2w256sbw4,
 ty_mpw256w32,
 ty_sbw4,
+ty_sw16w16,
+ty_sw32w32,
 ty_spbw256w64,
 ty_spbw256w256,
 ty_spw2w256sbw4,

C/primitive/elements/primitiveInitJet.inc

@@ -1,6 +1,9 @@
 /* This file has been automatically generated. */
+MK_JET(PARSE_SEQUENCE, 0x04b95bbeu, 0x881e1a6bu, 0x419f8288u, 0x3ff073eau, 0xdbc14f2cu, 0x8c56b36fu, 0x19dcecacu, 0x27e7737fu);
+MK_JET(CHECK_LOCK_HEIGHT, 0x04e9b61eu, 0x724e919au, 0xe008572bu, 0x9059f906u, 0xbfe9891eu, 0xdc6c67d3u, 0xde59c693u, 0xf20fa729u);
 MK_JET(SCALAR_MULTIPLY, 0x14513cf4u, 0x41179e62u, 0xfb4293bbu, 0x353ee5bfu, 0x01eddf8du, 0x81ce0310u, 0x062f09a8u, 0x1d2fbca8u);
 MK_JET(MULTIPLY_32, 0x161fd03au, 0x92c621b3u, 0x289849ffu, 0x29ad8134u, 0x99d63ed9u, 0x73db0e97u, 0x51785421u, 0xf568d18fu);
+MK_JET(CHECK_LOCK_DURATION, 0x1dc7eef9u, 0xd4c5afecu, 0x79a80eb0u, 0xef07186du, 0x458d0badu, 0x59606977u, 0x85450e10u, 0x7d5b5d8bu);
 MK_JET(GEJ_INFINITY, 0x2d9d36b4u, 0x6ead02dbu, 0x63b585dcu, 0xa67e5e4du, 0xcb940589u, 0xbb133c99u, 0x100d617cu, 0x27126e96u);
 MK_JET(SCALAR_IS_ZERO, 0x38a457cau, 0xb1c30c51u, 0x4e20e241u, 0xd5846540u, 0x75ec4d05u, 0x496c7e0bu, 0x1ce2de5eu, 0x2fc19916u);
 MK_JET(FULL_ADD_32, 0x4727361eu, 0xa003c1a4u, 0x83e57505u, 0xcf5b405au, 0x8227da1au, 0xddc47e2bu, 0x016c2d09u, 0xbe047fe8u);
@@ -13,8 +16,10 @@ MK_JET(SCALAR_ADD, 0x67e41fadu, 0x704500ceu, 0x97509132u, 0xd4f69734u, 0x2e8583e
 MK_JET(SCALAR_NEGATE, 0x6a976a67u, 0x68bd728fu, 0xe2105185u, 0x1c60eb25u, 0x72e5d06cu, 0x95566dfau, 0xe92820c8u, 0x424aaa4eu);
 MK_JET(FULL_SUBTRACT_32, 0x6d96f68au, 0x945c22e7u, 0x62115c09u, 0x4297b194u, 0xbedc0ce5u, 0xa0c92db6u, 0x4b830a18u, 0xb44df0d0u);
 MK_JET(GEJ_NEGATE, 0x71eeffb5u, 0xb637af51u, 0xc4978002u, 0xc212cdafu, 0x396cf8efu, 0xca33aab0u, 0xf833f81au, 0x9fb6a989u);
+MK_JET(CHECK_LOCK_DISTANCE, 0x7ed914c4u, 0x0bb3d23du, 0x678716c7u, 0xcfb6bf04u, 0x2095b010u, 0xb5506b9du, 0x413eea87u, 0x3cbc4fb0u);
 MK_JET(GEJ_ADD, 0x8075b590u, 0x28649087u, 0xded0e766u, 0x6e1a0051u, 0x4509d0c9u, 0x87d88d18u, 0x681ac89bu, 0xc960eb25u);
 MK_JET(GEJ_DOUBLE, 0x80d0825du, 0x57ce424cu, 0xc8b89dc2u, 0x510d7e65u, 0x858a994eu, 0x8e987623u, 0xd10e3483u, 0xde26df9eu);
+MK_JET(TX_LOCK_DURATION, 0x8526e3d4u, 0x3f43bd2bu, 0x4b1985c0u, 0xb9301d9au, 0x98290167u, 0xe587e5c3u, 0xcf135bc6u, 0xb1231346u);
 MK_JET(FE_NEGATE, 0x8766585du, 0x27d18863u, 0x42714443u, 0x2ba483b3u, 0x6cd2dd1fu, 0x36181410u, 0xacc71493u, 0x9c0cb56au);
 MK_JET(FE_SQUARE, 0x8e77cc8cu, 0x63693a2au, 0xcd9a6526u, 0x6a028906u, 0xf864214au, 0xf66ba54cu, 0xce11acb0u, 0x37c94393u);
 MK_JET(SCALAR_NORMALIZE, 0x90e02578u, 0x96990ba6u, 0xf0b07654u, 0x2919cd06u, 0x4ac08b27u, 0x7fae3479u, 0xe40918ebu, 0x6f5b07d8u);
@@ -29,10 +34,14 @@ MK_JET(FE_MULTIPLY, 0xac5a3626u, 0xb5fc2b5au, 0x206ac18fu, 0x1b0f9ecau, 0xcb5c63
 MK_JET(GEJ_NORMALIZE, 0xb41998deu, 0x564ef64fu, 0x63a4c9fau, 0xd1395064u, 0x832e7d5cu, 0x4c771d18u, 0x0fced28du, 0x8a765bd6u);
 MK_JET(FE_INVERT, 0xb6b11bd6u, 0x0258d326u, 0xb19b6f78u, 0x387ff3aau, 0xbf6a4c41u, 0x9d0c5a8du, 0xda6b4405u, 0x0bc6e9d5u);
 MK_JET(FE_NORMALIZE, 0xc070adbau, 0xab2c7be6u, 0xff577a75u, 0x07aff0e7u, 0x7657f309u, 0xe65d05fau, 0x23c19276u, 0xf73852ebu);
+MK_JET(CHECK_LOCK_TIME, 0xc073f616u, 0x84f3a6c2u, 0xe0273d05u, 0xb265477eu, 0x0094afe0u, 0x401e5e86u, 0x43981ee1u, 0x46588754u);
 MK_JET(FE_ADD, 0xc09d58e3u, 0x8dc4ce1au, 0xcc09dae8u, 0xa5881908u, 0xfe1ebc7fu, 0x1fc742c6u, 0x1cdc8493u, 0xf233b94au);
 MK_JET(SCALAR_INVERT, 0xc0e2ad1bu, 0xa6bfd910u, 0x4424f594u, 0xd0073ea1u, 0x99405e5cu, 0xa5b71283u, 0x94b613b9u, 0xe1bd36fcu);
 MK_JET(POINT_VERIFY_1, 0xc290db88u, 0xca696049u, 0x8d12e6e6u, 0x78be76c3u, 0x05279320u, 0x13384bf7u, 0x7c753628u, 0x78b842abu);
+MK_JET(TX_LOCK_DISTANCE, 0xccfdc62au, 0xed510ca0u, 0xdaeeffb5u, 0x0c6dabc1u, 0x1c03c40cu, 0x30c5c0fdu, 0xb5bb57a6u, 0xf5a8c2a3u);
 MK_JET(GEJ_Y_IS_ODD, 0xcf91c71du, 0xa71398ecu, 0x8c64fdbfu, 0x8fdc912eu, 0xd5a8c1fau, 0xc6566e0bu, 0x5913ebe9u, 0xc4b10617u);
+MK_JET(TX_LOCK_TIME, 0xd44ce14cu, 0xcfb3a1bcu, 0xb71210c0u, 0xa2e15bc9u, 0xf5c9a251u, 0x29a037beu, 0x483f16c3u, 0xa505db59u);
+MK_JET(PARSE_LOCK, 0xd5969c25u, 0xb56e87b4u, 0xfb2880eau, 0xee90cc94u, 0x49faa2f3u, 0xd0760de9u, 0xfee565dfu, 0xcf6a16c6u);
 MK_JET(SCALAR_SQUARE, 0xd636b49du, 0xc6b2266cu, 0xcecb7bc0u, 0x4168823bu, 0x2a5d7a1du, 0x2ac343dau, 0x605419d3u, 0x8dfdfde0u);
 MK_JET(GE_IS_ON_CURVE, 0xd9aa6606u, 0x5cb0ed2cu, 0x7168609du, 0xfd62ab64u, 0x3aa87c27u, 0xe0dbbf96u, 0xf2914528u, 0xfeef52c5u);
 MK_JET(GEJ_GE_ADD, 0xddc12bb2u, 0x89175ff5u, 0x87a570b3u, 0x02af6108u, 0xfa565bcau, 0xce9c374au, 0x10b78363u, 0x951daa64u);
@@ -44,4 +53,6 @@ MK_JET(LINEAR_VERIFY_1, 0xef106f25u, 0x25060debu, 0x6abe435bu, 0xb76ec3c6u, 0xe4
 MK_JET(SCALAR_MULTIPLY_LAMBDA, 0xf62400f5u, 0xbe7400a7u, 0x12e74a1du, 0xc1a841e6u, 0x024a9618u, 0x551c3364u, 0xc4e8156du, 0x1cdded83u);
 MK_JET(SUBTRACT_32, 0xf76ecad1u, 0xfda50f13u, 0x5bdfe3e5u, 0x33a15009u, 0x8f406261u, 0xc76f6dbfu, 0x6725f1e3u, 0x883c2ae2u);
 MK_JET(FE_SQUARE_ROOT, 0xf7718103u, 0x304cb436u, 0x96bdf92fu, 0x614c838du, 0x24d7dd7bu, 0xa8dc01abu, 0x5c6a7726u, 0x3c15f729u);
+MK_JET(TX_LOCK_HEIGHT, 0xf94f86a6u, 0xf07995ddu, 0xcdf8ccafu, 0xdeea8e58u, 0x450bcac4u, 0xde783597u, 0xf86ab089u, 0xeb64f7fcu);
 MK_JET(GEJ_RESCALE, 0xfa70aa15u, 0x3dab6bc9u, 0x9355c10cu, 0x61e5bfcfu, 0xa397b381u, 0xf7ef5915u, 0x9d83791au, 0x2a6a5824u);
+MK_JET(TX_IS_FINAL, 0xfe406277u, 0x096b0cd2u, 0x1cc383e0u, 0x110e244cu, 0x246f9571u, 0x05e94bb8u, 0x13ec75fbu, 0xebc97f92u);

C/primitive/elements/primitiveInitTy.inc

@@ -19,11 +19,14 @@
 (*bound_var)[ty_mmspbw256w64] = (unification_var){ .isBound = true, .bound = { .kind = SUM, .arg = { &(*bound_var)[ty_u], &(*bound_var)[ty_mspbw256w64] } }};
 (*bound_var)[ty_mmspbw256w256] = (unification_var){ .isBound = true, .bound = { .kind = SUM, .arg = { &(*bound_var)[ty_u], &(*bound_var)[ty_mspbw256w256] } }};
 (*bound_var)[ty_mmspw2w256sbw4] = (unification_var){ .isBound = true, .bound = { .kind = SUM, .arg = { &(*bound_var)[ty_u], &(*bound_var)[ty_mspw2w256sbw4] } }};
+(*bound_var)[ty_msw16w16] = (unification_var){ .isBound = true, .bound = { .kind = SUM, .arg = { &(*bound_var)[ty_u], &(*bound_var)[ty_sw16w16] } }};
 (*bound_var)[ty_mspbw256w64] = (unification_var){ .isBound = true, .bound = { .kind = SUM, .arg = { &(*bound_var)[ty_u], &(*bound_var)[ty_spbw256w64] } }};
 (*bound_var)[ty_mspbw256w256] = (unification_var){ .isBound = true, .bound = { .kind = SUM, .arg = { &(*bound_var)[ty_u], &(*bound_var)[ty_spbw256w256] } }};
 (*bound_var)[ty_mspw2w256sbw4] = (unification_var){ .isBound = true, .bound = { .kind = SUM, .arg = { &(*bound_var)[ty_u], &(*bound_var)[ty_spw2w256sbw4] } }};
 (*bound_var)[ty_mpw256w32] = (unification_var){ .isBound = true, .bound = { .kind = SUM, .arg = { &(*bound_var)[ty_u], &(*bound_var)[ty_pw256w32] } }};
 (*bound_var)[ty_sbw4] = (unification_var){ .isBound = true, .bound = { .kind = SUM, .arg = { &(*bound_var)[ty_b], &(*bound_var)[ty_w4] } }};
+(*bound_var)[ty_sw16w16] = (unification_var){ .isBound = true, .bound = { .kind = SUM, .arg = { &(*bound_var)[ty_w16], &(*bound_var)[ty_w16] } }};
+(*bound_var)[ty_sw32w32] = (unification_var){ .isBound = true, .bound = { .kind = SUM, .arg = { &(*bound_var)[ty_w32], &(*bound_var)[ty_w32] } }};
 (*bound_var)[ty_spbw256w64] = (unification_var){ .isBound = true, .bound = { .kind = SUM, .arg = { &(*bound_var)[ty_pbw256], &(*bound_var)[ty_w64] } }};
 (*bound_var)[ty_spbw256w256] = (unification_var){ .isBound = true, .bound = { .kind = SUM, .arg = { &(*bound_var)[ty_pbw256], &(*bound_var)[ty_w256] } }};
 (*bound_var)[ty_spw2w256sbw4] = (unification_var){ .isBound = true, .bound = { .kind = SUM, .arg = { &(*bound_var)[ty_pw2w256], &(*bound_var)[ty_sbw4] } }};