Re: [bitcoin-dev] Unlimited covenants, was Re: CHECKSIGFROMSTACK/{Verify} BIP for Bitcoin

[Billy Tetrud <billy.tetrud@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 11851 bytes --]

Thanks for the clarifications Sanket and Russel!

> OP_TWEAK

Ah gotcha. I'm very much in support of recursive covenants. I was lead to
them as a way to create more efficient and flexible wallet vaults. I
actually wrote a proposal
<https://github.com/fresheneesz/bip-efficient-bitcoin-vaults/blob/main/bip-pushoutputstack.md>
for an opcode to add state to an output. Its pretty useless without an
accompanying covenant opcode, but it seems a bit more straightforward than
the tricks you mentioned (op_tweak and otherwise). I don't plan on starting
a discussion on it yet tho, more work to be done on it and other things
to open discussion on first.

In any case, its nice to see so much general agreement on a topic that
could easily be embroidered in contention.

On Tue, Jul 6, 2021 at 9:26 PM ZmnSCPxj via bitcoin-dev <
bitcoin-dev@lists.linuxfoundation.org> wrote:

> Good morning Russell,
>
> > Hi ZmnSCPxj,
> >
> > I don't believe we need to ban Turing completeness for the sake of
> banning Turing completeness.
>
> Well I believe we should ban partial Turing-completeness, but allow total
> Turing-completeness.
>
> I just think that unlimited recursive covenants (with or without a
> convenient way to transform state at each iteration) are **not** partial
> Turing-complete, but *are* total Turing-complete. (^^)
>
> (The rest of this writeup is mostly programming languages nerdery so
> anyone who is not interested in Haskell (or purely functional programming)
> and programming language nerdery can feel free to skip the rest of this
> post.
> Basically, ZmnSCPxj thinks we should still ban Turing-completeness, but
> unbounded covenants get a pass because they are not, on a technicality,
> Turing-complete)
>
> For now, let us first taboo the term "Turing-complete", and instead focus
> on what I think matters here, the distinction between partial and total,
>
> In a total programming language we have a distinction between data and
> codata:
>
> * Data is defined according to its constructors, i.e. an algebraic data
> type.
> * Codata is defined according to its destructors, i.e. according to a
> "behavior" the codata has when a particular "action" is applied to it.
>
> For example, a singly-linked list data type would be defined as follows:
>
>     data List a where
>         Cons :: a -> List a -> List a
>         Nil :: List a
>
> On the other hand, an infinite codata stream of objects would be defined
> as follows:
>
>     codata Stream a where
>         head :: Stream a -> a
>         tail :: Stream a -> Stream a
>
> For `data` types, the result type for each constructor listed in the
> definition *must* be the type being defined.
> That is why `Cons` is declared as resulting in a `List a`.
> We declare data according to its constructors.
>
> For `codata` types, the *first argument* for each destructor listed in the
> definition *must* be the type being defined.
> That is why `head` accepts as its first argument the `Stream a` type.
>
> This is relevant because in a total function programming language, there
> exists some programming rule that restricts recursion.
> The simplest such restriction is substructural recursion:
>
> * If a function recurs:
>   * Every self-call should pass in a substructure of an argument as that
> argument.
>
> Every program that passes the above rule provably terminates.
> Since every recursion passes in a smaller part of an argument, eventually
> we will reach an indivisible primitive object being passed in, and
> processing will stop recursing and can return some value.
>
> Thus, a programing language that has substructural recursion rule check
> (and rejects programs that fail the substrucutral recursion check) are not
> "Turing-complete".
> The reason is that Turing-complete languages cannot solve the Halting
> Problem.
> But a language that includes the substructural recursion rule *does* have
> a Halting Problem solution: every program that passes the substructural
> recursion rule halts and the Halting Problem is decidable for all programs
> that pass the substructural recursion rule.
> (i.e. we are deliberately restricting ourselves to a subset of programs
> that pass substructural recursion, and reject programs that do not pass
> this rule as "not really programs", so every program halts)
>
> For example, the following definition of `mapList` is valid under
> substructural recursion:
>
>     mapList :: (a -> b) -> (List a -> List b)
>     mapList f Nil            = Nil
>     mapList f (Cons a as)    = Cons (f a) (mapList f as)
>
> The second sub-definition has a recursive call `mapList f as`.
> The second argument to that call, however, is a substructure of the second
> argument `Cons a as` on the LHS of the definition, thus it is a
> substructural recursive call, and accepted in a total programming language.
> *Every* recursion in `mapList` should then be a substructural call on the
> second argument of `mapList`.
>
> Now let us consider the following definition of `fibonacci`:
>
>     -- to use: fibonacci 1 1
>     fibonacci :: Integer -> Integer -> List Integer
>     fibonacci x y = Cons x (fibonacci y (x + y))
>
> The above is not substructural recursive, neither argument in the
> recursive `fibonacci y (x + y)` call is a substructure of the arguments in
> the LHS of the `fibonacci` definition `fibonacci x y`.
>
> Thus, we prevent certain unbounded computations like the above infinite
> sequence of fibonacci numbers.
>
> Now, let us consider a definition of `mapStream`, the similar function on
> streams, using copattern matching rather than pattern matching:
>
>     mapStream :: (a -> b) -> (Stream a -> Stream b)
>     head (mapStream f as) = f (head as)
>     tail (mapStream f as) = mapStream f (tail as)
>
> Now the interesting thing here is that in the substructural recursion
> check, what is being defined in the above stanza is ***not*** `mapStream`,
> but `head` and `tail`!
> Thus, it ignores the `mapStream f (tail as)`, because it is **not**
> recursion --- what is being defined here is `tail`.
>
> Looking at the above stanza, we can see that the `head` definition
> recurses, in the call `head as`.
> The first argument to `head as` is `as`, which is a substructure of the
> first argument of the LHS, `mapstream f as`.
> Similarly for the `tail` definition, there is a recursive call `tail as`
> which is substructural recursive, since the LHS has the first argument as
> `mapStream f as` and `as` is a substructure of that call.
>
> (Indeed, copatterns are an important advance in total programming
> languages, prior to copatterns people were bashing their heads trying to
> figure out a simple algorithm to ensure corecursion termination, and it
> turns out that copatterns make corecursion termination as trivial as
> substructural recursion on the destructurs)
>
> Now let us consider the following alternate definition of `fibonacci`
> which returns a `Stream Integer` rather than a `List Integer`:
>
>     fibonacci :: Integer -> Integer -> Stream Integer
>     head (fibonacci x y) = x
>     tail (fibonacci x y) = fibonacci y (x + y)
>
> The first definition `head (fibonacci x y) = ...` is nonrecursive.
> The sceon definition `tail (fibonacci x y) = ...` is ***also***
> nonrecursive because what is being defined is `tail`, and `tail` does not
> even appear in the RHS of the definition!
>
> With the syntax and its rules defined, let us now consider how to
> implement arbitrary-bound recursion in our total language.
>
> Let us define the following types:
>
>     data RecResult a where
>         Complete ::     a -> RecResult a
>         Continue :: Rec a -> RecResult a
>
>     codata Rec a where
>         step :: Rec a -> RecResult a
>
> `Rec a` is a monad:
>
>     instance Monad Rec where
>         step (return a) = Complete a
>         step (ma >>= f) = case (step ma) of
>                             Complete a   -> Continue (f a)
>                             Continue ma' -> Continue (ma' >>= f)
>         -- pretend we do not have the Haskellian `fail` ^^
>
> The definition of `step (ma >>= f)` is recursive, but it is a
> substructural recursion: we recurse on `(step ma)` but `ma` is a
> substructure of the first argument on the LHS, `ma >>= f`, thus the above
> still is provably corecursive terminating.
>
> The above is sufficient to define an infinite loop:
>
>     infiniteLoop :: Rec a
>     step infiniteLoop = Continue infiniteLoop
>
> The above is still accepted, since there is no recursion involved --- the
> RHS does not contain the function `step` being defined, thus no recursion.
>
> Now the important thing to note here is that the above `Rec` type is a
> perfectly fine definition for the Haskellian `IO` type.
>
> Then, the `main` program, of type `Rec ()`/`IO ()`, would then be passed
> to a driving function, written in C.
> This C function would replace the C-level `main` function, and would just
> call `step` on the Haskell-level `main`.
> If it results in `Complete ()`, the C function exits.
> If it results in `Continue ma`, then it calls `step` again on the `ma` and
> checks the result again, in a loop.
>
>     int main() {
>         HaskellObject* ma = haskell_get_main_function();
>         for (;;) {
>             HaskellObject* result = haskell_step(ma);
>             if (haskell_is_Complete(result))
>                  break;
>             ma = haskell_destructure_Continue(result);
>         }
>         return 0;
>     }
>
> The important point here is that *within* the total language, everything
> terminates.
> We put all the dirty non-termination "outside", in the C function that
> drives the entire processing, and have a very simple infinite loop in it
> that is easy to audit for correctness.
> Then, we can have significantly more confidence in the correctness of our
> program, since any infinite recursion would have to somehow resolve to some
> `IO` type, which explicitly allows for infinite recursion, and we can focus
> auditing on that part of the program alone.
>
> Similarly, when we consider recursive covenants, we note always that there
> has to be some external driving program, written in something other than
> Bitcoin SCRIPT, which will continuously create transactions that will keep
> returning the funds to the same covenant (plus or minus some state update).
> Otherwise, the funds will just sit there behind their protecting SCRIPT,
> just like every other UTXO owned by long-term HODLers.
>
> Such a program that continually pays a fund to "the same" covenant is no
> different, in principle, from the above C driving function for our
> total-functional-programming dialect of Haskell.
>
> Which is to say that I mostly agree with roconnor here (other than on
> exact definition of terms; I think my definition of "Turing-complete" is
> more restrictive than his, such that covenants are not in fact
> **technically** Turing-complete, but that is just semantics and I can live
> with that), I think that the recursive covenants in Bitcoin work
> equivalently to the `codata` types in total functional languages.
> As long as Bitcoin SCRIPT itself is provably terminating, I have no
> objections to the fact that we get arbitrary-bound processing by use of
> covenants, as they are "outside" the SCRIPT and have to be operated
> separately by a separate program.
>
> Indeed, we note as well that we can encode state in other parts of the TX
> anyway, so that we can write something more substantive than `while (true)
> { /* do nothing */ }`.
> So we might as well make it easy on us and just add `OP_TWEAK` (and maybe
> convenience opcodes for building Taproot Merkle trees?) as well.
>
>
> Regards,
> ZmnSCPxj
> _______________________________________________
> bitcoin-dev mailing list
> bitcoin-dev@lists.linuxfoundation.org
> https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev
>

[-- Attachment #2: Type: text/html, Size: 13175 bytes --]