Return-Path: Received: from smtp4.osuosl.org (smtp4.osuosl.org [IPv6:2605:bc80:3010::137]) by lists.linuxfoundation.org (Postfix) with ESMTP id 0970AC000E for ; Wed, 7 Jul 2021 04:26:41 +0000 (UTC) Received: from localhost (localhost [127.0.0.1]) by smtp4.osuosl.org (Postfix) with ESMTP id CE52040540 for ; Wed, 7 Jul 2021 04:26:40 +0000 (UTC) X-Virus-Scanned: amavisd-new at osuosl.org X-Spam-Flag: NO X-Spam-Score: -1.599 X-Spam-Level: X-Spam-Status: No, score=-1.599 tagged_above=-999 required=5 tests=[BAYES_00=-1.9, DKIM_SIGNED=0.1, DKIM_VALID=-0.1, DKIM_VALID_AU=-0.1, DKIM_VALID_EF=-0.1, FREEMAIL_FROM=0.001, FROM_LOCAL_NOVOWEL=0.5, RCVD_IN_MSPIKE_H4=0.001, RCVD_IN_MSPIKE_WL=0.001, SPF_HELO_PASS=-0.001, SPF_PASS=-0.001] autolearn=ham autolearn_force=no Authentication-Results: smtp4.osuosl.org (amavisd-new); dkim=pass (1024-bit key) header.d=protonmail.com Received: from smtp4.osuosl.org ([127.0.0.1]) by localhost (smtp4.osuosl.org [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id 9d57lthe3S5e for ; Wed, 7 Jul 2021 04:26:38 +0000 (UTC) X-Greylist: domain auto-whitelisted by SQLgrey-1.8.0 Received: from mail-40135.protonmail.ch (mail-40135.protonmail.ch [185.70.40.135]) by smtp4.osuosl.org (Postfix) with ESMTPS id 9074740375 for ; Wed, 7 Jul 2021 04:26:38 +0000 (UTC) Date: Wed, 07 Jul 2021 04:26:31 +0000 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=protonmail.com; s=protonmail; t=1625631994; bh=VdMlEN5tX1JEfC6JXm8zXUXomXN3Tn/uQBUgAv9T7W8=; h=Date:To:From:Cc:Reply-To:Subject:In-Reply-To:References:From; b=Ku1NtPFtvdFsJrYGHKJ/i5d0HEgs49pevGDuMuyuyKPqewHf3WBuzKDXazDBfOLyt XIue3VHvMF94R969hRE3uLcwF/UNiKSOQbzsI6mADOXaPwCQZA6k05InBH/6JQd5/j UJoEbbHE973K4sp65FTNTFmBJjyM6+Jrl+pIwI5g= To: Russell O'Connor From: ZmnSCPxj Reply-To: ZmnSCPxj Message-ID: In-Reply-To: References: <20210704011341.ddbiruuomqovrjn6@ganymede> <20210704203230.37hlpdyzr4aijiet@ganymede> <5keA_aPvmCO5yBh_mBQ6Z5SwnnvEW0T-3vahesaDh57f-qv4FbG1SFAzDvT3rFhre6kFl282VsxV_pynwn_CdvF7fzH2q9NW1ZQHPH1pmdo=@protonmail.com> MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Cc: Bitcoin Protocol Discussion Subject: Re: [bitcoin-dev] Unlimited covenants, was Re: CHECKSIGFROMSTACK/{Verify} BIP for Bitcoin X-BeenThere: bitcoin-dev@lists.linuxfoundation.org X-Mailman-Version: 2.1.15 Precedence: list List-Id: Bitcoin Protocol Discussion List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 07 Jul 2021 04:26:41 -0000 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