Date: Wed, 07 Jul 2021 04:26:31 +0000
To: Russell O'Connor <roconnor@blockstream.com>
From: ZmnSCPxj <ZmnSCPxj@protonmail.com>
Reply-To: ZmnSCPxj <ZmnSCPxj@protonmail.com>
Message-ID: <u2ETzW2-k7sjRKEz48C2n2QJvmWPVdhZIqtva_KvDNvxNDTVnR2zzYCL2Q8RUVkLm93OMJ2S2GOfUOxmdvNTaCIK1liebb4yvCCBBFB75f0=@protonmail.com>
In-Reply-To: <CAMZUoKnuRXNG1pyupHrL+Wo80TXTbADVrexoB=+BKC633v-qMw@mail.gmail.com>
References: <CAD5xwhjmu-Eee47Ho5eA6E6+aAdnchLU0OVZo=RTHaXnN17x8A@mail.gmail.com>
 <20210704011341.ddbiruuomqovrjn6@ganymede>
 <CAD5xwhimPBEV_tLpSPxs9B+XGUhvPx_dnhok=8=hyksyi4=B6g@mail.gmail.com>
 <20210704203230.37hlpdyzr4aijiet@ganymede>
 <5keA_aPvmCO5yBh_mBQ6Z5SwnnvEW0T-3vahesaDh57f-qv4FbG1SFAzDvT3rFhre6kFl282VsxV_pynwn_CdvF7fzH2q9NW1ZQHPH1pmdo=@protonmail.com>
 <CAMZUoKnuRXNG1pyupHrL+Wo80TXTbADVrexoB=+BKC633v-qMw@mail.gmail.com>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8
Content-Transfer-Encoding: quoted-printable
Cc: Bitcoin Protocol Discussion <bitcoin-dev@lists.linuxfoundation.org>
Subject: Re: [bitcoin-dev] Unlimited covenants,
	was Re: CHECKSIGFROMSTACK/{Verify} BIP for Bitcoin
Precedence: list

Good morning Russell,

> Hi ZmnSCPxj,
>
> I don't believe we need to ban Turing completeness for the sake of bannin=
g Turing completeness.

Well I believe we should ban partial Turing-completeness, but allow total T=
uring-completeness.

I just think that unlimited recursive covenants (with or without a convenie=
nt way to transform state at each iteration) are **not** partial Turing-com=
plete, 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 pr=
ogramming language nerdery can feel free to skip the rest of this post.
Basically, ZmnSCPxj thinks we should still ban Turing-completeness, but unb=
ounded 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 o=
n what I think matters here, the distinction between partial and total,

In a total programming language we have a distinction between data and coda=
ta:

* Data is defined according to its constructors, i.e. an algebraic data typ=
e.
* Codata is defined according to its destructors, i.e. according to a "beha=
vior" 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 defini=
tion *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 ex=
ists 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 ar=
gument.

Every program that passes the above rule provably terminates.
Since every recursion passes in a smaller part of an argument, eventually w=
e will reach an indivisible primitive object being passed in, and processin=
g will stop recursing and can return some value.

Thus, a programing language that has substructural recursion rule check (an=
d rejects programs that fail the substrucutral recursion check) are not "Tu=
ring-complete".
The reason is that Turing-complete languages cannot solve the Halting Probl=
em.
But a language that includes the substructural recursion rule *does* have a=
 Halting Problem solution: every program that passes the substructural recu=
rsion 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 tha=
t pass substructural recursion, and reject programs that do not pass this r=
ule as "not really programs", so every program halts)

For example, the following definition of `mapList` is valid under substruct=
ural recursion:

    mapList :: (a -> b) -> (List a -> List b)
    mapList f Nil            =3D Nil
    mapList f (Cons a as)    =3D 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 substructur=
al recursive call, and accepted in a total programming language.
*Every* recursion in `mapList` should then be a substructural call on the s=
econd 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 =3D 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 o=
f the `fibonacci` definition `fibonacci x y`.

Thus, we prevent certain unbounded computations like the above infinite seq=
uence of fibonacci numbers.

Now, let us consider a definition of `mapStream`, the similar function on s=
treams, using copattern matching rather than pattern matching:

    mapStream :: (a -> b) -> (Stream a -> Stream b)
    head (mapStream f as) =3D f (head as)
    tail (mapStream f as) =3D 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** recursi=
on --- 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 fir=
st argument of the LHS, `mapstream f as`.
Similarly for the `tail` definition, there is a recursive call `tail as` wh=
ich is substructural recursive, since the LHS has the first argument as `ma=
pStream 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 recurs=
ion 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) =3D x
    tail (fibonacci x y) =3D fibonacci y (x + y)

The first definition `head (fibonacci x y) =3D ...` is nonrecursive.
The sceon definition `tail (fibonacci x y) =3D ...` is ***also*** nonrecurs=
ive because what is being defined is `tail`, and `tail` does not even appea=
r 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) =3D Complete a
        step (ma >>=3D f) =3D case (step ma) of
                            Complete a   -> Continue (f a)
                            Continue ma' -> Continue (ma' >>=3D f)
        -- pretend we do not have the Haskellian `fail` ^^

The definition of `step (ma >>=3D f)` is recursive, but it is a substructur=
al recursion: we recurse on `(step ma)` but `ma` is a substructure of the f=
irst argument on the LHS, `ma >>=3D f`, thus the above still is provably co=
recursive terminating.

The above is sufficient to define an infinite loop:

    infiniteLoop :: Rec a
    step infiniteLoop =3D Continue infiniteLoop

The above is still accepted, since there is no recursion involved --- the R=
HS 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 perf=
ectly 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 c=
all `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 =3D haskell_get_main_function();
        for (;;) {
            HaskellObject* result =3D haskell_step(ma);
            if (haskell_is_Complete(result))
                 break;
            ma =3D haskell_destructure_Continue(result);
        }
        return 0;
    }

The important point here is that *within* the total language, everything te=
rminates.
We put all the dirty non-termination "outside", in the C function that driv=
es the entire processing, and have a very simple infinite loop in it that i=
s easy to audit for correctness.
Then, we can have significantly more confidence in the correctness of our p=
rogram, 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 Bi=
tcoin SCRIPT, which will continuously create transactions that will keep re=
turning the funds to the same covenant (plus or minus some state update).
Otherwise, the funds will just sit there behind their protecting SCRIPT, ju=
st like every other UTXO owned by long-term HODLers.

Such a program that continually pays a fund to "the same" covenant is no di=
fferent, in principle, from the above C driving function for our total-func=
tional-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 re=
strictive than his, such that covenants are not in fact **technically** Tur=
ing-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 objecti=
ons 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 s=
eparate program.

Indeed, we note as well that we can encode state in other parts of the TX a=
nyway, 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 c=
onvenience opcodes for building Taproot Merkle trees?) as well.


Regards,
ZmnSCPxj