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

[ZmnSCPxj <ZmnSCPxj@protonmail.com>]

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