--- Log opened Wed Feb 23 00:00:08 2022
01:03 -!- dr-orlovsky [~dr-orlovs@31.14.40.18] has quit [Quit: ZNC 1.8.0 - https://znc.in]
01:04 -!- dr-orlovsky [~dr-orlovs@31.14.40.18] has joined ##miniscript
04:46 < andytoshi> i think that would greatly complicate things to have a "negative" restriction
04:46 < andytoshi> then instead of B# requirements everywhere we'd have a B-not-$ requirement
04:46 < andytoshi> concept ACK # and B#
07:42 < jeremyrubin> So maybe we want a # type and a modifier (idk what letter) tonum: which could use e.g. op_size to cast to a B#?
10:00 < andytoshi> i don't think there's any opcode that can turn a B into a B#
10:15 <@sipa> OP_SIZE OP_NIP
10:16 <@sipa> or OP_0 OP_EQUAL for the negation
10:36 < andytoshi> ah yeah, if all you want is a boolean
12:50 < jeremyrubin> andytoshi more practically, there are operations like OP_IF B OP_ELSE B OP_ENDIF
12:50 < jeremyrubin> so if the input to OP_IF is OK to B, and not B#, then you can save the OP_SIZE/NIP thing
12:50 <@sipa> yeah, all arguments left on the stack by miniscript semantics are treated as booleans
12:51 <@sipa> at least in B expressions
12:51 <@sipa> maybe we should rename them to B=boolean
12:52 < jeremyrubin> maybe a good thing to add to tapscript
12:52 < jeremyrubin> OP_NONNULL
12:53 < jeremyrubin> {} -> {}, otherwise OP_1
12:58 < jeremyrubin> sipa I think it does kinda make sense to have B=boolean type and N=numeric type where N ==> B, but B =/=> N?
12:58 <@sipa> We don't have a (semantically) numeric type.
12:58 <@sipa> Only booleans, with different constraints on the allowed encodings.
12:59 <@sipa> Such constraints can be expressed using additional type properties.
12:59 < jeremyrubin> hm
12:59 < jeremyrubin> i think that's fair, you could have a B = boolean and S = strict boolean type?
12:59 < jeremyrubin> B = true is any nonnull, S = 4 bytes
13:00 < jeremyrubin> (and then the u type captures ultra-strict)
13:00 <@sipa> I don't see why you'd want to split it up. That'll complicate the specification of every fragment that accepts both.
13:01 <@sipa> Just add a type property in between () and u, which constrains to 4 bytes.
13:01 < jeremyrubin> so the # property again?
13:01 <@sipa> Yes.
13:01 < jeremyrubin> what's () in the context above?
13:01 <@sipa> ""
13:01 <@sipa> Nothing.
13:02 < jeremyrubin> u = unit, () also... unit sometimes :p
13:02 <@sipa> Haha.
13:02 <@sipa> I mean: we currently have B=4bytes Bu=0 or 1; the obvious solution is going to B=anything B#=4 bytes, B#u=0 or 1.
13:03 < jeremyrubin> fair, i think that's reasonable. B, boolean. B#u, unit, B# some number. Is Bu valid?
13:03 <@sipa> Bu would be valid as a type constraint, but it'd be practically equivalent to B#u.
13:03 <@sipa> Because # implies u.
13:03 < jeremyrubin> yep
13:03 <@sipa> Eh, the other way around.
13:03 < jeremyrubin> yep
13:06 < jeremyrubin> what would be the next step for implementing this spec change?
13:06 <@sipa> I'd first like to get all the rest that's in flight done, and integration into core.
13:07 <@sipa> Too many concurrent changes becomes unwieldy.
13:07 < jeremyrubin> fair
13:07 <@sipa> We also have the whole raw*() stuff, the question of n-ary and_v, and_b, or_b, ... musig2 integration though that's mostly independent at least.
13:08 < jeremyrubin> one consideration, revisiting a little
13:08 < jeremyrubin> if we did add a NN type (not null)
13:08 < jeremyrubin> then i could make CTV NN without drop
13:08 < jeremyrubin> err
13:08 < jeremyrubin> not not null... 
13:09 < jeremyrubin> 'Value'
13:09 <@sipa> hmm, the # lets you do that, no?
13:09 < jeremyrubin> make B ==> 'Value'
13:09 <@sipa> ctv(X) would map to <X> OP_CTV, and have type B.
13:09 < jeremyrubin> and then make the IF clauses take Value
13:09 < jeremyrubin> yes, i'm thinking more from a software engineering perspective
13:10 <@sipa> like after/older
13:10 < jeremyrubin> the patches to the system might be smaller if we add a Value type 
13:10 <@sipa> that would very much surprise me
13:10 < jeremyrubin> because only CTV (for my fork) would require the new Value type, whereas adding # i have to change all of miniscript
13:11 <@sipa> i don't care about CTV :p
13:11 < jeremyrubin> that's a you problem
13:11 <@sipa> i want # to enable after/older with timestamps > 2^31
13:11 < jeremyrubin> people are playing with it on signet already so i am thinking through how to improve it
13:11 <@sipa> i just mean: ctv isn't the main reason for wanting this - we want this # (or something equivalent) anyway
13:12 < jeremyrubin> yes fair point
13:12 < jeremyrubin> my point is that Value is equivalent, and contains the patches to just the CTV/older/after part
13:12 < jeremyrubin> v.s. changing the type output of all clauses
13:12 <@sipa> that's not true
13:12 < jeremyrubin> (not all, many/most)
13:13 <@sipa> any fragment that keeps working with unrestricted value would have its definition changed
13:13 < jeremyrubin> ah
13:13 < jeremyrubin> sure
13:13 < jeremyrubin> I guess it's a question of changing input types v.s. changing output types and input types?
13:13 <@sipa> e.g. and_b and or_b would require B, not B#
13:14 <@sipa> which means that we could actually get away without a new fragment for converting B to B#; and_b(0,X) works.
13:14 <@sipa> eh, and_b(1,X) or or_b(0,X)
13:15 <@sipa> oh, no, that doesn't typecheck; it'd need to be and_b(1,a:X) or and_b(X,s:1), which is more opcodes
13:16 <@sipa> arguably a Bz could be used in any place a W is expected
13:16 <@sipa> which would fix this
13:18 <@sipa> an explicit wrapper for converting B to B# is easier
13:26 < jeremyrubin> hm
13:26 < jeremyrubin> i'll need to review the fragments
14:09 -!- dr_orlovsky [~dr-orlovs@31.14.40.18] has joined ##miniscript
14:09 -!- dr-orlovsky [~dr-orlovs@31.14.40.18] has quit [Quit: ZNC 1.8.0 - https://znc.in]
23:15 -!- devrandom [~devrandom@2001:470:69fc:105::d4d] has quit [Quit: Reconnecting]
23:15 -!- devrandom [~devrandom@2001:470:69fc:105::d4d] has joined ##miniscript
23:50 < darosior> "arguably a Bz could be used in any place a W is expected" -> Interesting. Looks like it works and could lead to smaller scripts when a timelock is used.
--- Log closed Thu Feb 24 00:00:08 2022