path: root/e3/e2bc73850f36d10d4871b1d0480a95c5833123

Return-Path: <fresheneesz@gmail.com>
Received: from smtp2.osuosl.org (smtp2.osuosl.org [140.211.166.133])
 by lists.linuxfoundation.org (Postfix) with ESMTP id C31D5C000E
 for <bitcoin-dev@lists.linuxfoundation.org>;
 Wed,  7 Jul 2021 06:12:44 +0000 (UTC)
Received: from localhost (localhost [127.0.0.1])
 by smtp2.osuosl.org (Postfix) with ESMTP id B18CF4049F
 for <bitcoin-dev@lists.linuxfoundation.org>;
 Wed,  7 Jul 2021 06:12:44 +0000 (UTC)
X-Virus-Scanned: amavisd-new at osuosl.org
X-Spam-Flag: NO
X-Spam-Score: -2.099
X-Spam-Level: 
X-Spam-Status: No, score=-2.099 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,
 HTML_MESSAGE=0.001, RCVD_IN_DNSWL_NONE=-0.0001, SPF_PASS=-0.001]
 autolearn=ham autolearn_force=no
Authentication-Results: smtp2.osuosl.org (amavisd-new);
 dkim=pass (2048-bit key) header.d=gmail.com
Received: from smtp2.osuosl.org ([127.0.0.1])
 by localhost (smtp2.osuosl.org [127.0.0.1]) (amavisd-new, port 10024)
 with ESMTP id ydt-F-BYvZsF
 for <bitcoin-dev@lists.linuxfoundation.org>;
 Wed,  7 Jul 2021 06:12:43 +0000 (UTC)
X-Greylist: whitelisted by SQLgrey-1.8.0
Received: from mail-ej1-x636.google.com (mail-ej1-x636.google.com
 [IPv6:2a00:1450:4864:20::636])
 by smtp2.osuosl.org (Postfix) with ESMTPS id A301840121
 for <bitcoin-dev@lists.linuxfoundation.org>;
 Wed,  7 Jul 2021 06:12:42 +0000 (UTC)
Received: by mail-ej1-x636.google.com with SMTP id b2so1444610ejg.8
 for <bitcoin-dev@lists.linuxfoundation.org>;
 Tue, 06 Jul 2021 23:12:42 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025;
 h=mime-version:references:in-reply-to:from:date:message-id:subject:to
 :cc; bh=u7YuivvuTUeKlCaiDmTehtG6/pPIKKcxyafm/Xi7Mss=;
 b=AEejDojs45i4AQKoy3xyCgtYHAI/LqirU5vbGnH5GL0Jaq2ShmlDaEUfHC9utxY3qm
 y4RFwwnQbcwvgcH9jf4FwjccpUYXRi7Aq+Pvvw/J/C/tV6rvjsBEpzdMWZOeRPFNOgJ3
 1mDbBC3lGvH2eBdHUlH5STPXbPbgAhNolLP73NSPN5lnBHDFDkxbHsIi4Chd+DfzaHAa
 N9XiVW17LD8/eIvAaF4SvOVemZVxMgh3kY8b/Yegni6U5DizbyPZ+Itue6ikdoyUyKbI
 fSW7fnazZOUdSlGA2MjLXay0NaIV3hXwAtnGsE45jS7AUcX501TU9uRaaaw1mblDT6n+
 lahA==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
 d=1e100.net; s=20161025;
 h=x-gm-message-state:mime-version:references:in-reply-to:from:date
 :message-id:subject:to:cc;
 bh=u7YuivvuTUeKlCaiDmTehtG6/pPIKKcxyafm/Xi7Mss=;
 b=fDYxiIea9lynw8bqMcrFsF5jOFPStDBYk0PoaaHU7xMwa/hN1g3CzEH7Jd6j31jMQQ
 vksso+tOyXgaIjPrQkj9d1uzKKrKgWHhz5ViUgKDj/3dq6X7gnehIYvNOmFbGnvzeVWV
 vtEgfajF+uaQnmLbDLtv7BG8KecEBCu+GFI705+pnpJGZfBl6Yx2sYZaEnXKmv/w3ngK
 kzY8jPLjWrzhgH06BpI065PqvimH+bW/ognxupGOvezcNfp6OLaCeEuWStNFxfj6mwkc
 zsXXUCgl30M5ZpSBAaXmbzoO02nf0LnRuoscdR237zoyXsPPautJ3qK0C7yMpWF89+7U
 IKWg==
X-Gm-Message-State: AOAM532HJjW3fcoLN6R4BX4Bc9oGb4kD0MDWeG1oeZDqBGMlL27yGsTW
 cM7b1D7hibXdkIIgdjH4pd/YaevZrjwwdD733AI=
X-Google-Smtp-Source: ABdhPJwBUa4j76aPsTs75dEac1t+0Kr7RMdtl4TWQDwl6cSQYAXJHXIW1zkmsVoNv+fvR7/6wpsc2U9L1A2X+XkUwU0=
X-Received: by 2002:a17:907:9622:: with SMTP id
 gb34mr22527907ejc.401.1625638360824; 
 Tue, 06 Jul 2021 23:12:40 -0700 (PDT)
MIME-Version: 1.0
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>
 <u2ETzW2-k7sjRKEz48C2n2QJvmWPVdhZIqtva_KvDNvxNDTVnR2zzYCL2Q8RUVkLm93OMJ2S2GOfUOxmdvNTaCIK1liebb4yvCCBBFB75f0=@protonmail.com>
In-Reply-To: <u2ETzW2-k7sjRKEz48C2n2QJvmWPVdhZIqtva_KvDNvxNDTVnR2zzYCL2Q8RUVkLm93OMJ2S2GOfUOxmdvNTaCIK1liebb4yvCCBBFB75f0=@protonmail.com>
From: Billy Tetrud <billy.tetrud@gmail.com>
Date: Tue, 6 Jul 2021 23:12:24 -0700
Message-ID: <CAGpPWDZJ8CbsV+c7vt5w9Ejfa5dER19-uaLL4hKeaiogL1uixA@mail.gmail.com>
To: ZmnSCPxj <ZmnSCPxj@protonmail.com>, 
 Bitcoin Protocol Discussion <bitcoin-dev@lists.linuxfoundation.org>
Content-Type: multipart/alternative; boundary="00000000000007bf3e05c6826dcf"
X-Mailman-Approved-At: Wed, 07 Jul 2021 08:20:40 +0000
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 <bitcoin-dev.lists.linuxfoundation.org>
List-Unsubscribe: <https://lists.linuxfoundation.org/mailman/options/bitcoin-dev>, 
 <mailto:bitcoin-dev-request@lists.linuxfoundation.org?subject=unsubscribe>
List-Archive: <http://lists.linuxfoundation.org/pipermail/bitcoin-dev/>
List-Post: <mailto:bitcoin-dev@lists.linuxfoundation.org>
List-Help: <mailto:bitcoin-dev-request@lists.linuxfoundation.org?subject=help>
List-Subscribe: <https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev>, 
 <mailto:bitcoin-dev-request@lists.linuxfoundation.org?subject=subscribe>
X-List-Received-Date: Wed, 07 Jul 2021 06:12:44 -0000

--00000000000007bf3e05c6826dcf
Content-Type: text/plain; charset="UTF-8"

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
>

--00000000000007bf3e05c6826dcf
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr">Thanks for the clarifications Sanket and Russel!<div><br><=
/div><div>&gt; OP_TWEAK</div><div><br></div><div>Ah gotcha. I&#39;m very mu=
ch 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 href=3D"htt=
ps://github.com/fresheneesz/bip-efficient-bitcoin-vaults/blob/main/bip-push=
outputstack.md">a proposal</a> 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&#39;t plan on starting a discussion on it yet tho, more work to=C2=
=A0be done on it and other things to=C2=A0open discussion on first.</div><d=
iv><br></div><div>In any case, its nice to see so much general agreement on=
 a topic that could easily be embroidered=C2=A0in contention.=C2=A0</div></=
div><br><div class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_attr">On=
 Tue, Jul 6, 2021 at 9:26 PM ZmnSCPxj via bitcoin-dev &lt;<a href=3D"mailto=
:bitcoin-dev@lists.linuxfoundation.org">bitcoin-dev@lists.linuxfoundation.o=
rg</a>&gt; wrote:<br></div><blockquote class=3D"gmail_quote" style=3D"margi=
n:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex=
">Good morning Russell,<br>
<br>
&gt; Hi ZmnSCPxj,<br>
&gt;<br>
&gt; I don&#39;t believe we need to ban Turing completeness for the sake of=
 banning Turing completeness.<br>
<br>
Well I believe we should ban partial Turing-completeness, but allow total T=
uring-completeness.<br>
<br>
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. (^^)<br>
<br>
(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.<br>
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)<br>
<br>
For now, let us first taboo the term &quot;Turing-complete&quot;, and inste=
ad focus on what I think matters here, the distinction between partial and =
total,<br>
<br>
In a total programming language we have a distinction between data and coda=
ta:<br>
<br>
* Data is defined according to its constructors, i.e. an algebraic data typ=
e.<br>
* Codata is defined according to its destructors, i.e. according to a &quot=
;behavior&quot; the codata has when a particular &quot;action&quot; is appl=
ied to it.<br>
<br>
For example, a singly-linked list data type would be defined as follows:<br=
>
<br>
=C2=A0 =C2=A0 data List a where<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0 Cons :: a -&gt; List a -&gt; List a<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0 Nil :: List a<br>
<br>
On the other hand, an infinite codata stream of objects would be defined as=
 follows:<br>
<br>
=C2=A0 =C2=A0 codata Stream a where<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0 head :: Stream a -&gt; a<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0 tail :: Stream a -&gt; Stream a<br>
<br>
For `data` types, the result type for each constructor listed in the defini=
tion *must* be the type being defined.<br>
That is why `Cons` is declared as resulting in a `List a`.<br>
We declare data according to its constructors.<br>
<br>
For `codata` types, the *first argument* for each destructor listed in the =
definition *must* be the type being defined.<br>
That is why `head` accepts as its first argument the `Stream a` type.<br>
<br>
This is relevant because in a total function programming language, there ex=
ists some programming rule that restricts recursion.<br>
The simplest such restriction is substructural recursion:<br>
<br>
* If a function recurs:<br>
=C2=A0 * Every self-call should pass in a substructure of an argument as th=
at argument.<br>
<br>
Every program that passes the above rule provably terminates.<br>
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.<br>
<br>
Thus, a programing language that has substructural recursion rule check (an=
d rejects programs that fail the substrucutral recursion check) are not &qu=
ot;Turing-complete&quot;.<br>
The reason is that Turing-complete languages cannot solve the Halting Probl=
em.<br>
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.<br>
(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 &quot;not really programs&quot;, so every program halts)<br>
<br>
For example, the following definition of `mapList` is valid under substruct=
ural recursion:<br>
<br>
=C2=A0 =C2=A0 mapList :: (a -&gt; b) -&gt; (List a -&gt; List b)<br>
=C2=A0 =C2=A0 mapList f Nil=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =3D Ni=
l<br>
=C2=A0 =C2=A0 mapList f (Cons a as)=C2=A0 =C2=A0 =3D Cons (f a) (mapList f =
as)<br>
<br>
The second sub-definition has a recursive call `mapList f as`.<br>
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.<br>
*Every* recursion in `mapList` should then be a substructural call on the s=
econd argument of `mapList`.<br>
<br>
Now let us consider the following definition of `fibonacci`:<br>
<br>
=C2=A0 =C2=A0 -- to use: fibonacci 1 1<br>
=C2=A0 =C2=A0 fibonacci :: Integer -&gt; Integer -&gt; List Integer<br>
=C2=A0 =C2=A0 fibonacci x y =3D Cons x (fibonacci y (x + y))<br>
<br>
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`.<br>
<br>
Thus, we prevent certain unbounded computations like the above infinite seq=
uence of fibonacci numbers.<br>
<br>
Now, let us consider a definition of `mapStream`, the similar function on s=
treams, using copattern matching rather than pattern matching:<br>
<br>
=C2=A0 =C2=A0 mapStream :: (a -&gt; b) -&gt; (Stream a -&gt; Stream b)<br>
=C2=A0 =C2=A0 head (mapStream f as) =3D f (head as)<br>
=C2=A0 =C2=A0 tail (mapStream f as) =3D mapStream f (tail as)<br>
<br>
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`!<br>
Thus, it ignores the `mapStream f (tail as)`, because it is **not** recursi=
on --- what is being defined here is `tail`.<br>
<br>
Looking at the above stanza, we can see that the `head` definition recurses=
, in the call `head as`.<br>
The first argument to `head as` is `as`, which is a substructure of the fir=
st argument of the LHS, `mapstream f as`.<br>
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.<br>
<br>
(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)<br>
<br>
Now let us consider the following alternate definition of `fibonacci` which=
 returns a `Stream Integer` rather than a `List Integer`:<br>
<br>
=C2=A0 =C2=A0 fibonacci :: Integer -&gt; Integer -&gt; Stream Integer<br>
=C2=A0 =C2=A0 head (fibonacci x y) =3D x<br>
=C2=A0 =C2=A0 tail (fibonacci x y) =3D fibonacci y (x + y)<br>
<br>
The first definition `head (fibonacci x y) =3D ...` is nonrecursive.<br>
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!<br>
<br>
With the syntax and its rules defined, let us now consider how to implement=
 arbitrary-bound recursion in our total language.<br>
<br>
Let us define the following types:<br>
<br>
=C2=A0 =C2=A0 data RecResult a where<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0 Complete ::=C2=A0 =C2=A0 =C2=A0a -&gt; RecResul=
t a<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0 Continue :: Rec a -&gt; RecResult a<br>
<br>
=C2=A0 =C2=A0 codata Rec a where<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0 step :: Rec a -&gt; RecResult a<br>
<br>
`Rec a` is a monad:<br>
<br>
=C2=A0 =C2=A0 instance Monad Rec where<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0 step (return a) =3D Complete a<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0 step (ma &gt;&gt;=3D f) =3D case (step ma) of<b=
r>
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=
=A0 =C2=A0 =C2=A0 =C2=A0 Complete a=C2=A0 =C2=A0-&gt; Continue (f a)<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=
=A0 =C2=A0 =C2=A0 =C2=A0 Continue ma&#39; -&gt; Continue (ma&#39; &gt;&gt;=
=3D f)<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0 -- pretend we do not have the Haskellian `fail`=
 ^^<br>
<br>
The definition of `step (ma &gt;&gt;=3D f)` is recursive, but it is a subst=
ructural recursion: we recurse on `(step ma)` but `ma` is a substructure of=
 the first argument on the LHS, `ma &gt;&gt;=3D f`, thus the above still is=
 provably corecursive terminating.<br>
<br>
The above is sufficient to define an infinite loop:<br>
<br>
=C2=A0 =C2=A0 infiniteLoop :: Rec a<br>
=C2=A0 =C2=A0 step infiniteLoop =3D Continue infiniteLoop<br>
<br>
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.<b=
r>
<br>
Now the important thing to note here is that the above `Rec` type is a perf=
ectly fine definition for the Haskellian `IO` type.<br>
<br>
Then, the `main` program, of type `Rec ()`/`IO ()`, would then be passed to=
 a driving function, written in C.<br>
This C function would replace the C-level `main` function, and would just c=
all `step` on the Haskell-level `main`.<br>
If it results in `Complete ()`, the C function exits.<br>
If it results in `Continue ma`, then it calls `step` again on the `ma` and =
checks the result again, in a loop.<br>
<br>
=C2=A0 =C2=A0 int main() {<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0 HaskellObject* ma =3D haskell_get_main_function=
();<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0 for (;;) {<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 HaskellObject* result =3D haskell=
_step(ma);<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 if (haskell_is_Complete(result))<=
br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0break;<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 ma =3D haskell_destructure_Contin=
ue(result);<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0 }<br>
=C2=A0 =C2=A0 =C2=A0 =C2=A0 return 0;<br>
=C2=A0 =C2=A0 }<br>
<br>
The important point here is that *within* the total language, everything te=
rminates.<br>
We put all the dirty non-termination &quot;outside&quot;, 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.<br>
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.<br>
<br>
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).<b=
r>
Otherwise, the funds will just sit there behind their protecting SCRIPT, ju=
st like every other UTXO owned by long-term HODLers.<br>
<br>
Such a program that continually pays a fund to &quot;the same&quot; covenan=
t is no different, in principle, from the above C driving function for our =
total-functional-programming dialect of Haskell.<br>
<br>
Which is to say that I mostly agree with roconnor here (other than on exact=
 definition of terms; I think my definition of &quot;Turing-complete&quot; =
is more restrictive than his, such that covenants are not in fact **technic=
ally** 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.<br>
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 &quot;outside&quot; the SCRIPT and have to be operated separat=
ely by a separate program.<br>
<br>
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 */ }`.<br>
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.<br>
<br>
<br>
Regards,<br>
ZmnSCPxj<br>
_______________________________________________<br>
bitcoin-dev mailing list<br>
<a href=3D"mailto:bitcoin-dev@lists.linuxfoundation.org" target=3D"_blank">=
bitcoin-dev@lists.linuxfoundation.org</a><br>
<a href=3D"https://lists.linuxfoundation.org/mailman/listinfo/bitcoin-dev" =
rel=3D"noreferrer" target=3D"_blank">https://lists.linuxfoundation.org/mail=
man/listinfo/bitcoin-dev</a><br>
</blockquote></div>

--00000000000007bf3e05c6826dcf--