Last active
September 5, 2023 09:55
-
-
Save dgpv/b57ecf4d9e3d0bfdcc2eb9147c9b9abf to your computer and use it in GitHub Desktop.
This file contains hidden or 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