Last active
September 5, 2023 09:55
-
-
Save dgpv/b57ecf4d9e3d0bfdcc2eb9147c9b9abf to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
============ | |
Valid paths: | |
============ | |
IF NUMEQUAL(5, tx_num_outputs) @ 48:L130 : True | |
IF wit5 @ 171:L317 : True | |
----------------------------------------------- | |
IF NUMEQUAL(5, tx_num_outputs) @ 48:L130 : True | |
IF wit5 @ 171:L317 : False | |
----------------------------------------------- | |
IF NUMEQUAL(5, tx_num_outputs) @ 48:L130 : False | |
IF wit5 @ 171:L317 : True | |
------------------------------------------------ | |
IF NUMEQUAL(5, tx_num_outputs) @ 48:L130 : False | |
IF wit5 @ 171:L317 : False | |
------------------------------------------------ | |
============================== | |
Enforced constraints per path: | |
============================== | |
All valid paths: | |
---------------- | |
NUMEQUAL(2, tx_num_inputs) @ 2:L46 | |
EQUAL(1, INPUT_1_ASSET_PREFIX) @ 6:L54 | |
EQUAL($lbtcAsset, INPUT_1_ASSET) @ 11:L62 | |
EQUAL(INPUT_0_SPK_WITVER, OUTPUT_0_SPK_WITVER) @ 17:L73 | |
EQUAL(INPUT_0_SPK_WITPROG, OUTPUT_0_SPK_WITPROG) @ 18:L74 | |
EQUAL(1, OUTPUT_1_ASSET_PREFIX) @ 22:L86 | |
EQUAL($synthAsset, OUTPUT_1_ASSET) @ 24:L88 | |
EQUAL(1, OUTPUT_2_ASSET_PREFIX) @ 28:L97 | |
EQUAL(INPUT_1_ASSET, OUTPUT_2_ASSET) @ 29:L99 | |
EQUAL(1, OUTPUT_2_VALUE_PREFIX) @ 33:L104 | |
EQUAL($bondAmount, OUTPUT_2_VALUE) @ 35:L106 | |
EQUAL(1, OUTPUT_3_ASSET_PREFIX) @ 39:L112 | |
EQUAL(INPUT_1_ASSET, OUTPUT_3_ASSET) @ 40:L114 | |
CHECKSIGFROMSTACK(wit3, SHA256(&oracle_tag.wit1.wit2.$currencyCode), &oracle_xpub) @ 80:L179 | |
<*> EQUAL(1, OUTPUT_1_VALUE_PREFIX) @ 84:L185 | |
NUMEQUAL(32, SIZE(wit4)) @ 113:L224 | |
NUMEQUAL(1, OUTPUT_1_SPK_WITVER) @ 185:L336 | |
NUMEQUAL(1, OUTPUT_2_SPK_WITVER) @ 190:L341 | |
EQUAL(OUTPUT_1_SPK_WITPROG, OUTPUT_2_SPK_WITPROG) @ 191:L343 | |
<*> 1 @ END | |
IF NUMEQUAL(5, tx_num_outputs) @ 48:L130 : True | |
----------------------------------------------- | |
{*} LESSTHANOREQUAL(tx_num_outputs, 5) @ 45:L126 | |
EQUAL(1, OUTPUT_4_ASSET_PREFIX) @ 52:L135 | |
EQUAL(INPUT_1_ASSET, OUTPUT_4_ASSET) @ 53:L137 | |
IF NUMEQUAL(5, tx_num_outputs) @ 48:L130 : False | |
------------------------------------------------ | |
LESSTHANOREQUAL(tx_num_outputs, 5) @ 45:L126 | |
IF wit5 @ 171:L317 : True | |
------------------------- | |
TWEAKVERIFY(wit6.OUTPUT_1_SPK_WITPROG, SHA256(&TT_tag.$claimCovenantInternalXpub.SHA256(&TB_tag.&leafhash_cov_sr.&leafhash_cov_sb)), $claimCovenantInternalXpub) @ 208:L364 | |
IF wit5 @ 171:L317 : False | |
-------------------------- | |
TWEAKVERIFY(wit6.OUTPUT_1_SPK_WITPROG, SHA256(&TT_tag.$claimCovenantInternalXpub.SHA256(&TB_tag.&leafhash_cov_sb.&leafhash_cov_sr)), $claimCovenantInternalXpub) @ 208:L364 | |
Data references: | |
---------------- | |
oracle_tag = SHA256($oracleMessageTag).SHA256($oracleMessageTag) | |
oracle_xpub = SUBSTR($oracleXPubsArray, LSHIFT(wit0, 5), 32) | |
TT_tag = SHA256('TapTweak/elements').SHA256('TapTweak/elements') | |
TB_tag = SHA256('TapBranch/elements').SHA256('TapBranch/elements') | |
leafhash_cov_sr = SHA256(&TL_tag.x('c4').&DATA_sr_covenant) | |
TL_tag = SHA256('TapLeaf/elements').SHA256('TapLeaf/elements') | |
DATA_sr_covenant = SUBSTR(SIZE(&sr_covenant), 0, 1).&sr_covenant | |
sr_covenant = &DATA_minter_xpub.&DATA_lbtc_coll_amount.$claimReleaseCovenantTail | |
DATA_minter_xpub = SIZE(wit4).wit4 | |
DATA_lbtc_coll_amount = SIZE(&lbtc_coll_amount).&lbtc_coll_amount | |
lbtc_coll_amount = QUOTIENT(DIV64(&synth_coll_amount_scaled, wit2)) | |
synth_coll_amount_scaled = MUL64(&synth_coll_amount, SCRIPTNUMTOLE64($precisionScaler)) | |
synth_coll_amount = ADD64(OUTPUT_1_VALUE, QUOTIENT(DIV64(OUTPUT_1_VALUE, SCRIPTNUMTOLE64(2)))) | |
leafhash_cov_sb = SHA256(&TL_tag.x('c4').&DATA_sb_covenant) | |
DATA_sb_covenant = SIZE(&sb_covenant).&sb_covenant | |
sb_covenant = &DATA_burn_cov_args.$claimBurnCovenantTail | |
DATA_burn_cov_args = &DATA_synth_asset.&DATA_o1_amount.&DATA_burn_ts | |
DATA_synth_asset = SIZE(OUTPUT_1_ASSET).OUTPUT_1_ASSET | |
DATA_o1_amount = SIZE(OUTPUT_1_VALUE).OUTPUT_1_VALUE | |
DATA_burn_ts = SIZE(&burn_ts).&burn_ts | |
burn_ts = ADD64($synthBurnDelay, wit1) | |
====================== | |
Model values per path: | |
====================== | |
IF NUMEQUAL(5, tx_num_outputs) @ 48:L130 : True | |
IF wit5 @ 171:L317 : True | |
----------------------------------------------- | |
wit0 : x('') | |
wit1 : le64(3459450621994925057) | |
wit2 : le64(-70808553123808257) | |
wit3 : x('') | |
wit4 : x('eaebec7ced7deeeff0f1f27e7f80f381f4f5f68283f7f8f9fafbfcfdfe84ff00') | |
wit5 = 1 | |
wit6 : x('') | |
INPUT_1_ASSET : x('d731d832d9da33dbdc34dd35dedfe0e1363738e2e339e43ae5e6e7e83b3c3de9') | |
INPUT_1_ASSET_PREFIX = x('01') | |
INPUT_0_SPK_WITPROG : x('d5d6') | |
INPUT_0_SPK_WITVER : x('06') | |
OUTPUT_0_SPK_WITPROG : x('d5d6') | |
OUTPUT_1_SPK_WITPROG : x('0240413e42434445464748493f4a4b4c4d4e4f505152535455565758595a5b5c5d') | |
OUTPUT_2_SPK_WITPROG : x('0240413e42434445464748493f4a4b4c4d4e4f505152535455565758595a5b5c5d') | |
OUTPUT_0_SPK_WITVER : x('06') | |
OUTPUT_1_SPK_WITVER = 1 | |
OUTPUT_2_SPK_WITVER = 1 | |
OUTPUT_2_VALUE : x('7374757677787a79') | |
OUTPUT_1_VALUE : le64(1) | |
OUTPUT_2_VALUE_PREFIX = x('01') | |
OUTPUT_1_VALUE_PREFIX = x('01') | |
OUTPUT_1_ASSET : x('69ffb55ab8c81c21f58b2adcb0835a08608af59d042f033764339cd8e6ba33e7') | |
OUTPUT_2_ASSET : x('d731d832d9da33dbdc34dd35dedfe0e1363738e2e339e43ae5e6e7e83b3c3de9') | |
OUTPUT_3_ASSET : x('d731d832d9da33dbdc34dd35dedfe0e1363738e2e339e43ae5e6e7e83b3c3de9') | |
OUTPUT_4_ASSET : x('d731d832d9da33dbdc34dd35dedfe0e1363738e2e339e43ae5e6e7e83b3c3de9') | |
OUTPUT_1_ASSET_PREFIX = x('01') | |
OUTPUT_2_ASSET_PREFIX = x('01') | |
OUTPUT_3_ASSET_PREFIX = x('01') | |
OUTPUT_4_ASSET_PREFIX = x('01') | |
tx_num_inputs = 2 | |
tx_num_outputs = 5 | |
<result> = 1 | |
IF NUMEQUAL(5, tx_num_outputs) @ 48:L130 : True | |
IF wit5 @ 171:L317 : False | |
----------------------------------------------- | |
wit0 : x('') | |
wit1 : le64(70931694147665922) | |
wit2 : le64(359447956157104387) | |
wit3 : x('') | |
wit4 : x('5152e9eaeb53ec54ed55eeef565758f0595a5bf1f25cf3f45d5e5f6061f5f6f7') | |
wit5 = 0 | |
wit6 : x('0279be667ef9dcbbac55a06295ce870b07029bfcdb2dce28d959f2815b16f8') | |
INPUT_1_ASSET : x('f081fa7c4fd96a8101d59ecedef324c4027b9cbc39735d254b48d88dd065d6e3') | |
INPUT_1_ASSET_PREFIX = x('01') | |
INPUT_0_SPK_WITPROG : x('cdb0') | |
INPUT_0_SPK_WITVER : x('04') | |
OUTPUT_0_SPK_WITPROG : x('cdb0') | |
OUTPUT_1_SPK_WITPROG : x('1798') | |
OUTPUT_2_SPK_WITPROG : x('1798') | |
OUTPUT_0_SPK_WITVER : x('04') | |
OUTPUT_1_SPK_WITVER = 1 | |
OUTPUT_2_SPK_WITVER = 1 | |
OUTPUT_2_VALUE : x('8384858687888a89') | |
OUTPUT_1_VALUE : le64(1) | |
OUTPUT_2_VALUE_PREFIX = x('01') | |
OUTPUT_1_VALUE_PREFIX = x('01') | |
OUTPUT_1_ASSET : x('f8f9fafbfcfdfeff000102030405060708090a0b0c0d0e0f1011121314151617') | |
OUTPUT_2_ASSET : x('f081fa7c4fd96a8101d59ecedef324c4027b9cbc39735d254b48d88dd065d6e3') | |
OUTPUT_3_ASSET : x('f081fa7c4fd96a8101d59ecedef324c4027b9cbc39735d254b48d88dd065d6e3') | |
OUTPUT_4_ASSET : x('f081fa7c4fd96a8101d59ecedef324c4027b9cbc39735d254b48d88dd065d6e3') | |
OUTPUT_1_ASSET_PREFIX = x('01') | |
OUTPUT_2_ASSET_PREFIX = x('01') | |
OUTPUT_3_ASSET_PREFIX = x('01') | |
OUTPUT_4_ASSET_PREFIX = x('01') | |
tx_num_inputs = 2 | |
tx_num_outputs = 5 | |
<result> = 1 | |
IF NUMEQUAL(5, tx_num_outputs) @ 48:L130 : False | |
IF wit5 @ 171:L317 : True | |
------------------------------------------------ | |
wit0 : x('') | |
wit1 : le64(-143838119701774593) | |
wit2 : le64(-1) | |
wit3 : x('') | |
wit4 : x('d8d9daa7a8a9aaabacadaeafb0b1b2b3b4b5b6b7b8b9babbbcbdbebfc0c1c2c3') | |
wit5 = 1 | |
wit6 : x('03999a9b9c9d9e9fa0a1a2a3a4a5a6a7a8a9aaab373836393a3b3c3d3e3f40') | |
INPUT_1_ASSET : x('a03722abcb0d54aa9e6b3893e9f8137d9060219c42cc139c32c2eb67080d73c6') | |
INPUT_1_ASSET_PREFIX = x('01') | |
INPUT_0_SPK_WITPROG : x('1112') | |
INPUT_0_SPK_WITVER : x('0e') | |
OUTPUT_0_SPK_WITPROG : x('1112') | |
OUTPUT_1_SPK_WITPROG : x('5267') | |
OUTPUT_2_SPK_WITPROG : x('5267') | |
OUTPUT_0_SPK_WITVER : x('0e') | |
OUTPUT_1_SPK_WITVER = 1 | |
OUTPUT_2_SPK_WITVER = 1 | |
OUTPUT_2_VALUE : x('868788898a8b8d8c') | |
OUTPUT_1_VALUE : le64(1) | |
OUTPUT_2_VALUE_PREFIX = x('01') | |
OUTPUT_1_VALUE_PREFIX = x('01') | |
OUTPUT_1_ASSET : x('d7d8d9dadbdcddc1dedfe0e1e2e3e4e5e6e7e8e9eaebecedeeeff0f1f2f3f4f5') | |
OUTPUT_2_ASSET : x('a03722abcb0d54aa9e6b3893e9f8137d9060219c42cc139c32c2eb67080d73c6') | |
OUTPUT_3_ASSET : x('a03722abcb0d54aa9e6b3893e9f8137d9060219c42cc139c32c2eb67080d73c6') | |
OUTPUT_1_ASSET_PREFIX = x('01') | |
OUTPUT_2_ASSET_PREFIX = x('01') | |
OUTPUT_3_ASSET_PREFIX = x('01') | |
tx_num_inputs = 2 | |
tx_num_outputs = 4 | |
<result> = 1 | |
IF NUMEQUAL(5, tx_num_outputs) @ 48:L130 : False | |
IF wit5 @ 171:L317 : False | |
------------------------------------------------ | |
wit0 : x('') | |
wit1 : le64(-115001875011505579) | |
wit2 : le64(-39565473168199065) | |
wit3 : x('') | |
wit4 : x('b1b2b3b4b5b6b7b8b9babbbcbdbebfc0c1c2c3c4c5c6c7c8c9cacbcccdcecfd0') | |
wit5 = 0 | |
wit6 : x('03a8bec6bfc0c7c8c9cacbccc1c2c3c4c5cd') | |
INPUT_1_ASSET : x('f081fa7c4fd96a8101d59ecedef324c4027b9cbc39735d254b48d88dd065d6e3') | |
INPUT_1_ASSET_PREFIX = x('01') | |
INPUT_0_SPK_WITPROG : x('7879') | |
INPUT_0_SPK_WITVER : x('04') | |
OUTPUT_0_SPK_WITPROG : x('7879') | |
OUTPUT_1_SPK_WITPROG : x('0192939495969798999a9b9c9d9e9f') | |
OUTPUT_2_SPK_WITPROG : x('0192939495969798999a9b9c9d9e9f') | |
OUTPUT_0_SPK_WITVER : x('04') | |
OUTPUT_1_SPK_WITVER = 1 | |
OUTPUT_2_SPK_WITVER = 1 | |
OUTPUT_2_VALUE : x('77787a7b7c7d7f7e') | |
OUTPUT_1_VALUE : le64(968018677887232) | |
OUTPUT_2_VALUE_PREFIX = x('01') | |
OUTPUT_1_VALUE_PREFIX = x('01') | |
OUTPUT_1_ASSET : x('d1d2d3d4d5d6d7d8d9dadbdcdddedfe0e1e2e3e4e5e6e7e8e9eaebecedeeeff0') | |
OUTPUT_2_ASSET : x('f081fa7c4fd96a8101d59ecedef324c4027b9cbc39735d254b48d88dd065d6e3') | |
OUTPUT_3_ASSET : x('f081fa7c4fd96a8101d59ecedef324c4027b9cbc39735d254b48d88dd065d6e3') | |
OUTPUT_1_ASSET_PREFIX = x('01') | |
OUTPUT_2_ASSET_PREFIX = x('01') | |
OUTPUT_3_ASSET_PREFIX = x('01') | |
tx_num_inputs = 2 | |
tx_num_outputs = 4 | |
<result> = 1 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment