--- Log opened Thu Mar 18 00:00:59 2021 02:02 -!- gnusha [~gnusha@unaffiliated/kanzure/bot/gnusha] has quit [Ping timeout: 264 seconds] 02:02 -!- gnusha [~gnusha@unaffiliated/kanzure/bot/gnusha] has joined ##miniscript 02:02 [Users ##miniscript] 02:02 [ achow101 ] [ kallewoof ] 02:02 [ aj ] [ matt2 ] 02:02 [ andytoshi ] [ meshcollider ] 02:02 [ appservicebot5] [ michaelfolkson] 02:02 [ darosior ] [ midnight ] 02:02 [ digi_james ] [ nothingmuch ] 02:02 [ dr-orlovsky ] [ notmandatory ] 02:02 [ elichai2 ] [ robot-dreams ] 02:02 [ felixweis ] [ RubenSomsen ] 02:02 [ ghost43_ ] [ sanket1729 ] 02:02 [ gnusha ] [ sanketcell_ ] 02:02 [ gwillen ] [ schmidty ] 02:02 [ harding ] [ sgeisler ] 02:02 [ hugohn ] [ shesek ] 02:02 [ jb55 ] [ sipa ] 02:02 [ jeremyrubin ] [ willcl_ark ] 02:02 [ jnewbery ] [ windsok ] 02:02 [ justinmoon_ ] 02:02 -!- Irssi: ##miniscript: Total of 35 nicks [0 ops, 0 halfops, 0 voices, 35 normal] 02:03 -!- Channel ##miniscript created Fri Jul 5 15:35:47 2019 02:05 -!- Irssi: Join to ##miniscript was synced in 159 secs 07:46 -!- jonatack [~jon@37.164.254.128] has joined ##miniscript 08:17 < darosior> andytoshi, sanket1729: So http://bitcoin.sipa.be/miniscript/ says that for thresh 1 < k < n, but we actually are more laxist in rust-bitcoin and allow 1 <= k <= n 08:17 < darosior> Was writing a patch but we seem to force only keys in multi() 08:19 < darosior> Ok, sorry for the ping we should be using and() to emulate thresh(n, "n sub policies") .. 09:02 < darosior> Hmm so in the compiler we actually *have* to translate thresh(1, A, B, ...) in or()s 09:14 < andytoshi> ;/win 20 09:14 < andytoshi> oops :) 09:19 -!- roconnor [~roconnor@host-45-58-230-226.dyn.295.ca] has joined ##miniscript 09:33 < jeremyrubin> darosior: IMO it is better to use thresh than a tree of and / or because you pass off to the policy compiler an object which requires fewer allocations 09:33 < jeremyrubin> at some point the compilation can be optimized to avoid translating into the and/or tree 11:10 < darosior> jeremyrubin: but the point is that we do avoid it right now and it's not compiling valid (according to the 'reference' and the C++ implem) Miniscript 11:11 < jeremyrubin> it's explicitly supported in rust-miniscript 11:11 < jeremyrubin> I think it's even been floated to drop And/Or in favor of just having threshold 11:12 < sipa> in policy or in miniscript? 11:12 < jeremyrubin> sipa: was just gonna ask that 11:12 < sipa> i have no idea what you're talking about! 11:13 < sipa> afaik the type rules for thresh in miniscript are incorrect with k=1 or k=n, but i don't remember exactly 11:13 < darosior> sipa: yes that was my initial point, we don't respect that in rust-bitcoin 11:14 < darosior> jeremyrubin: i'm talking about Miniscript, not policy: thresh is invalid for k==1 or k==n http://bitcoin.sipa.be/miniscript/ 11:14 < sipa> sanketcell_, andytoshi: do you remember? 11:16 < sipa> i can't immediately see why that would be the case, though 11:16 < sipa> but it's been a while since i thought about it 11:16 < jeremyrubin> let me check and see if I have logs of where we discussed this prev 11:16 < jeremyrubin> Monday July 13 2020? 11:18 < jeremyrubin> july 20 too 11:18 < jeremyrubin> [Monday, July 20, 2020] [11:35:15 AM PDT] but i also want to support n-ary or/and, which will complicate things further 11:18 < jeremyrubin> [Monday, July 20, 2020] [11:35:36 AM PDT] oh, this also means that in abstract policies you don't really need and/or, as they're exactly identical to thresh(1,...) or thresh(n,...) 11:19 < jeremyrubin> I think the issue is that if you have k = 1 or k = n maybe it's ambiguous with And / Or? 11:20 < sipa> in abstract policies yes 11:20 < sipa> there is no difference between 1-of-N and and/or 11:20 < sipa> this discussion is about miniscript, not policies 11:20 < sipa> in miniscript: different fragments means different scripts 11:21 < jeremyrubin> https://github.com/sipa/miniscript/issues/39 11:22 < sipa> i'm happy to adjust the spec to permit thresh with k=1 or k=n, but i want to see a good argument that all type properties hold 11:26 < jeremyrubin> anywasy w.r.t. darosior's question, 11:26 < jeremyrubin> [Monday, July 20, 2020] [12:15:10 PM PDT] We are supporting 1 and n for thresh. 11:26 < jeremyrubin> so it seems that support for k=1, k=n is explicitly done in rust-miniscript 11:26 < jeremyrubin> you should follow up with sanket1729 for the proof of correctness 11:26 < sipa> yes, we know 11:30 < jeremyrubin> isnt' thresh(3, a,b, c) equiv to thresh(3, a, b, c, false)? 11:31 < sipa> in policyland, yes 11:31 < sipa> in miniscriptland, no 11:31 < jeremyrubin> Ah sure, I just mean in terms of properties in miniscript land 11:31 < jeremyrubin> the types should be the same, no? 11:31 < sipa> that depends on what type properties a,b,c have 11:32 < andytoshi> sipa: i think we disallowed k==1 and k==n purely for moral "it's always less efficient" reasons 11:32 < andytoshi> there are type issues with k==0 11:32 < sipa> andytoshi: that's possible 11:32 < andytoshi> always less effecient than and_b/or_b 11:33 < sipa> if that's all there is to it, i'm happy to permit k=1 k=n 11:33 < andytoshi> all things being equal, i think we ought to allow it ... though i don't care enough to work through convincing you/myself that it's ok :P 11:33 < jeremyrubin> btw for k=1, thresh(1, a,b,c) == thresh(2, a,b,c,true) 11:34 < andytoshi> well, k==n i'm very confident about, i don't see how n and n-1 could be meaningfully different from a type pow 11:34 < jeremyrubin> (just in terms of logically you can construct something with the same satisfiability0 11:34 < andytoshi> jeremyrubin: semantically yes 11:34 < andytoshi> k==1 i'd have to think about, then you have one B and zero Ws, and possibly we need at least one W for some reason 11:34 < andytoshi> also k==n==1 may be broken even if k==1 is otherwise ok ... i don't remember 11:34 < sipa> jeremyrubin: miniscript type properties have nothing to do with semantics/satisfiability 11:35 < sipa> they are about the corresponding bitcoin script being legal/safe/secure/nonmalleable 11:37 < sipa> andytoshi: yeah, i think if we swap in all the reasoning we did to construct the type properties in the first place, this will be obvious 11:37 < sipa> the issue isn't reasoning about it, it's remembering everything :) 11:37 < sipa> formal proofs would be nice... 11:38 < jeremyrubin> sipa: sure, I'm just trying to think of how -- short of an implementation bug -- something with a clearly non malleable satisfier (base unit type) that can be elided for logical equivalence could cause an issue 11:38 < jeremyrubin> but perhaps such triangulation isn't useful here 11:38 < sipa> jeremyrubin: or_b(a,true) is malleable while a isn't 11:39 < sipa> hmm that's a bad example 11:40 < jeremyrubin> thresh(3, true, false, true, false, true, true, true) is malleable? 11:40 < sipa> yes 11:40 < sipa> or_b(a,b) and or_c(a,b) are clearly semantically equivalent 11:41 < sipa> but or_b(a,b) is malleable if b does not have the "e" property 11:41 < sipa> while or_c(a,b) isn't 11:46 < andytoshi> sipa: heh, dmitry did something close to a formal proof 11:46 < andytoshi> but i never understood it 11:46 < sipa> same 12:10 -!- willcl_ark [~quassel@unaffiliated/willcl-ark/x-8282106] has quit [Remote host closed the connection] 12:12 -!- willcl_ark [~quassel@unaffiliated/willcl-ark/x-8282106] has joined ##miniscript 12:51 -!- jonatack_ [~jon@37.173.214.42] has joined ##miniscript 12:52 -!- jonatack [~jon@37.164.254.128] has quit [Ping timeout: 245 seconds] 16:10 -!- jonatack_ [~jon@37.173.214.42] has quit [Ping timeout: 240 seconds] --- Log closed Fri Mar 19 00:00:00 2021