From mboxrd@z Thu Jan 1 00:00:00 1970 Delivery-date: Sat, 18 Apr 2026 14:49:29 -0700 Received: from mail-oa1-f61.google.com ([209.85.160.61]) by mail.fairlystable.org with esmtps (TLS1.3) tls TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256 (Exim 4.94.2) (envelope-from ) id 1wEDXc-0006ks-Ua for bitcoindev@gnusha.org; Sat, 18 Apr 2026 14:49:29 -0700 Received: by mail-oa1-f61.google.com with SMTP id 586e51a60fabf-415e1ea16b4sf3314630fac.1 for ; Sat, 18 Apr 2026 14:49:28 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1776548962; cv=pass; d=google.com; s=arc-20240605; b=C10ChyiClA3Pt7A9MJL0o7bJh47TLDBelJutqb5rZoOoukolKnenaC3GL6NcF8FZKf it/AQunKGDaTfSD2f0EGLfTNSU8JK05/a0EaYxkVn49qxejSDU1SXunAV6zGgGDOhKJB u5u5meo0t6CA3BDXM0mrgL+M1/EjJHe7tKh8zbqj2LyaRKRTSLDTuSrTcmyr0ArwwSGS Jfqv+IqBdXYExBrFYCuo7kk13Hvrcq/IPLntVVXXDEMJ6AOc6q+sx3DuDUKzU0KxF2fr YRgkxOH0kLto6KtpZJHip1+NawuB0DAjxUIA9a7ia+X74bsbp8PzZjNYaddjIjMsnOvh EKvA== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20240605; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:content-language:thread-index :content-transfer-encoding:mime-version:message-id:date:subject :in-reply-to:references:to:from:sender:dkim-signature; bh=KkCuZ2bAZazfFpBSlIiWaAUiVra3p4ZdQhCrszJVt4M=; fh=QRyYg/IW+TfdjBYqig97LwkUV3/qM5q1+8FjVGWTMvQ=; b=YOOVVXBppspC2ZxOrTLvlSfkrC635DIjz8CkSJIDCSQPpdbv+I8ZoJEvIISwBg8fI6 O1Ur+FddTGh+4C6vlXdn/IYT3nZh2lUflv4FGJOoVmAc9dPS49Exnn4gQnXx+GBnwd08 HFIpNt0kleU4s+Wg011zgcv1a11OQl803eVDQPfmjwZknkaLBV/vRo1ex3zYWL3zAELy u1xs1erQn2bZQQDcqCRT5xNGPACtPEnyDI5p0RS3ETRMX0xc0rW/A6bWw1WbugtNZ+2T Q5cHPt8N/dpRF+NnEj5XSp0SoPEx6edR3jAIUzyYEeQahuSRlVKdg+PR/OQS1GuVt078 5abw==; darn=gnusha.org ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@voskuil.org header.s=google header.b=jV1sIwwD; spf=pass (google.com: domain of eric@voskuil.org designates 2607:f8b0:4864:20::f31 as permitted sender) smtp.mailfrom=eric@voskuil.org; dara=pass header.i=@googlegroups.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20251104; t=1776548962; x=1777153762; darn=gnusha.org; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:content-language:thread-index :content-transfer-encoding:mime-version:message-id:date:subject :in-reply-to:references:to:from:sender:from:to:cc:subject:date :message-id:reply-to; bh=KkCuZ2bAZazfFpBSlIiWaAUiVra3p4ZdQhCrszJVt4M=; b=A6hD02IxNv63bGrX6IXzvTg/AQiGv+xnJTuLesqZWbqCPwTX5KjbuPRpOa1uD8EwHA +jI5vYeJ6IS/6eRVCU08TTVxWnTM4d3vU6b2STCeV0EGLs10BwsEl1K3FyYhWP+XgbFg CEDF2ikg8oXMZ5JpYxEmOBhVPJukohO4ctZ/MQRHZLvT8/PmwfZc61rm0GgrsYfjOM5+ COf01blzrDZDZUiKsziy/G+RTQlrPMh8AHCncPl2LRTJ2ygl4Mkc9DbHr32U8QQTYzsQ nF+yKVfdGduEPaqxcEJG0/kfz1NBVOZcCvOHQYSXSKgY2tTQ0E8Zfm8H4sJpZb0AnFE5 DkXA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20251104; t=1776548962; x=1777153762; h=list-unsubscribe:list-subscribe:list-archive:list-help:list-post :list-id:mailing-list:precedence:x-original-authentication-results :x-original-sender:content-language:thread-index :content-transfer-encoding:mime-version:message-id:date:subject :in-reply-to:references:to:from:x-gm-gg:x-beenthere :x-gm-message-state:sender:from:to:cc:subject:date:message-id :reply-to; bh=KkCuZ2bAZazfFpBSlIiWaAUiVra3p4ZdQhCrszJVt4M=; b=HJJ14jaX8IRFM7PdyjirIIv/efL8gvMqdSaASazECgpYS7ksON0N3qRrESX8K5XcTF 3ltOCP78nPDbhkIAO7KuOwWFaB5Oi7izEqB4PXkAhABQE3nlqZhJw4QmRrtBidHGyR+j N8IQLuwZgWx39hTWc7dwqhGu1EGdxMWuLONOza69sZXa2eLacIw2RWHyo6lvSArtW7CZ Ao9MqE1p9aG0bneS7GmFPo6v0tRlvHcqoxWaSyUx8gQbOf4WfZJ9acPsYwJy1x+dS3H7 BLnu5IBXRY1JkxaMaMRW8Z5QgkIJQyCAGH1WHy748QAAia1dKNn95b0layOdxPF0PS5e 7eLA== Sender: bitcoindev@googlegroups.com X-Forwarded-Encrypted: i=2; AFNElJ+5SDiB13++vSnJCJcLAJ5Do+2ENssGoKXInMPGuSuUO0enKiW/sTDQV1Wvsuq9uth7lorNW3YEdIWX@gnusha.org X-Gm-Message-State: AOJu0YwbhmCceFV7E+Yux4H+XJO756rgIHIliol4sJJutyeWL69FEbxG 59bNVprpGRwjRLwwNA3Hgw10Bd1PEwNgcjZgvoUzF71U9kjcK0jL5rvR X-Received: by 2002:a4a:edc4:0:b0:67b:a667:f53e with SMTP id 006d021491bc7-69462e29e56mr4320926eaf.1.1776548962196; Sat, 18 Apr 2026 14:49:22 -0700 (PDT) X-BeenThere: bitcoindev@googlegroups.com; h="AYAyTiLCAXFUKcBKIjlgPUO+4mFo3a5njvOAbQRyN2GXUDMJxQ==" Received: by 2002:a05:6820:1689:b0:67d:fa47:dad3 with SMTP id 006d021491bc7-6943cccf616ls1530062eaf.2.-pod-prod-03-us; Sat, 18 Apr 2026 14:49:17 -0700 (PDT) X-Forwarded-Encrypted: i=2; AFNElJ9YG4fRJLG7ILU8mnFKAndNUoGX5bym6cHYq5rPltar2KdkxZvUII+nlpLV+FtsL+j1V+C4MMnq4xh1@googlegroups.com X-Received: by 2002:a05:6808:1b25:b0:460:f435:2a70 with SMTP id 5614622812f47-4799cab417cmr4545606b6e.47.1776548957193; Sat, 18 Apr 2026 14:49:17 -0700 (PDT) Received: by 2002:a05:6808:64a:b0:479:ad2b:104b with SMTP id 5614622812f47-479ad2b1215msb6e; Sat, 18 Apr 2026 14:15:12 -0700 (PDT) X-Forwarded-Encrypted: i=2; AFNElJ8U/9aRCrNhp9MNiYAvz8tS85+9h1gxfYNVfH6O9jUQCzbSrUghNilFOgqv6cG6EmvUaDZD2YAj6IO9@googlegroups.com X-Received: by 2002:a17:90a:da83:b0:35b:9ab6:1d4b with SMTP id 98e67ed59e1d1-3614048e368mr8579569a91.20.1776546911598; Sat, 18 Apr 2026 14:15:11 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1776546911; cv=none; d=google.com; s=arc-20240605; b=CRex3ZtuXKUtHCwhhRjCMXAaMZgmziBpupd0p6mub9ix6aX3BaujbwpI9M2l/U5M27 tBxutQhbPjgyN5LIiHgSIX+pJ0AMu4XynZBIJhStEtereTiZ0dh0F4mNDNGmfPQz/XJR OUvwO0CkXH2cro7dshiJqzzVygGyPIcMYQIYYm8msaqPXW3+b+jza4dB257bpkr0xe4B g7ydWX2ewGRJh2BI3hwvJskyFmNbYvMLIa1FKiIPYQq5ii3IrmyNDXJ38rLbcsPJcdAY jTzmNConMjc1MBODNXDQy7LjqzaRsBAwemv2wjMWMg3w3scfZYFXYLxsmF5234RLsVGz MMkg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20240605; h=content-language:thread-index:content-transfer-encoding :mime-version:message-id:date:subject:in-reply-to:references:to:from :dkim-signature; bh=wegczzN9F9YhBMX1n4Trn5FESRS1gYK9GUyeZ7oxAKc=; fh=o77leyrNgINi1wGKgpsLVodm3F7fPbfxL781OwOt9fY=; b=iuI7wCj3s11/EuRt2BzUKp/lNVB0RTz56C9gW5sPo50OnRjt1gjMRQ1ceK2OqrbHI4 64eKHGSKLqUsUmFKzr82y6F037IB1esHTp1UM05bI4r9rgvy3pYjt2hJBvUHMFIFDI/J KW3iaMIz41ILHffmaVOa97Eg8CivYlXaPqLBxgPFGNUodmre6met7XFURDX/lqI3jObY uNItDpEjFaRlGFxECAFRcGkr2ghDI74rLS7tFCVDe1BsQvsOfmxcvMkrlRcbpyxVOqSB mfd97iaVMqjTh1p632A1to5vSypmZBd+ZhFt7kfkEyEuyXA0ZjJoiSePb/QBpwzHJ5MF XSrg==; dara=google.com ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@voskuil.org header.s=google header.b=jV1sIwwD; spf=pass (google.com: domain of eric@voskuil.org designates 2607:f8b0:4864:20::f31 as permitted sender) smtp.mailfrom=eric@voskuil.org; dara=pass header.i=@googlegroups.com Received: from mail-qv1-xf31.google.com (mail-qv1-xf31.google.com. [2607:f8b0:4864:20::f31]) by gmr-mx.google.com with ESMTPS id 98e67ed59e1d1-3613fa67d28si129987a91.1.2026.04.18.14.15.11 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sat, 18 Apr 2026 14:15:11 -0700 (PDT) Received-SPF: pass (google.com: domain of eric@voskuil.org designates 2607:f8b0:4864:20::f31 as permitted sender) client-ip=2607:f8b0:4864:20::f31; Received: by mail-qv1-xf31.google.com with SMTP id 6a1803df08f44-8acb7f2586bso21844796d6.1 for ; Sat, 18 Apr 2026 14:15:11 -0700 (PDT) X-Forwarded-Encrypted: i=1; AFNElJ9gRZQPGfCiM0zlqRbSj2tvSuLrPvTIjHl7x2qJUTAfJ/RrQVIc2X+nsGD84w4ET8EPgOSsLk7q29AR@googlegroups.com X-Gm-Gg: AeBDiet/5INvaiERyFe2Lr+paHyM06FU0/EMungWBV2m9N8jWd6WFNOrlc4jeqm6I0h 6+yOP5jFccKiV2ukogFKDovnto7qY7iO7xPom2cPByocULwDmMCF+2ZFdkLDqJTxwgcvy/1Y6CW m8jVRJSFq8r9SIuVF3Mkyua/LaYK5VA2MckrGZ7yL6sIHSiAwegR0GzrQAzacMeYZn1QwCo0d4o tL1ldsvbR4qW1CjGmNrbL/TPgVBqQtY9pdPFLLq9/gcqcDutN5lkd/8o0J1tpv4n6x4E1E0kbGt 9XZ6UFaVnFyCf2RV9jZQqDnij5un0zgPAnuMWqyV4w/B2sqgLJG8EjHNiwinFwhKvzEBDOME2Tp 7aBVbhZeScwf3ybbZjJKm/ay4VjpPhJoUwNhaaIKzWHLYk2De/gM/wypfhkx9Y+uSvqaX22Z7ad DXnKTTi9394nuMIhLB0q3wc42dAml0yHs4H+cPqyO/GPmBVDWdOQpuTAiqAD+3ZFNUPDkQ6Ubj/ n8ZnwlD4XCkT88= X-Received: by 2002:ad4:574c:0:b0:8ac:a6f7:8a6c with SMTP id 6a1803df08f44-8b0281d58c8mr124577036d6.36.1776546910096; Sat, 18 Apr 2026 14:15:10 -0700 (PDT) Received: from ERICDESKTOP (c-73-100-212-73.hsd1.nh.comcast.net. [73.100.212.73]) by smtp.gmail.com with ESMTPSA id 6a1803df08f44-8b02ac72915sm42218416d6.15.2026.04.18.14.15.09 (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Sat, 18 Apr 2026 14:15:09 -0700 (PDT) From: To: "'Toby Sharp'" , "'Bitcoin Development Mailing List'" References: <4cd864f3-96dd-4058-bfcd-b1bbf6cfa269n@googlegroups.com> <006501dccd36$ea035fd0$be0a1f70$@voskuil.org> In-Reply-To: Subject: RE: [bitcoindev] Hornet Update: A declarative executable specification of Bitcoin consensus rules Date: Sat, 18 Apr 2026 17:15:07 -0400 Message-ID: <00b401dccf78$6f5e7a00$4e1b6e00$@voskuil.org> MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Mailer: Microsoft Outlook 16.0 Thread-Index: AQIM7pKi29ODGLwkBcXlBApwgU5LuwFCflclAfG4G9i1a07AwA== Content-Language: en-us X-Original-Sender: eric@voskuil.org X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@voskuil.org header.s=google header.b=jV1sIwwD; spf=pass (google.com: domain of eric@voskuil.org designates 2607:f8b0:4864:20::f31 as permitted sender) smtp.mailfrom=eric@voskuil.org; dara=pass header.i=@googlegroups.com Precedence: list Mailing-list: list bitcoindev@googlegroups.com; contact bitcoindev+owners@googlegroups.com List-ID: X-Google-Group-Id: 786775582512 List-Post: , List-Help: , List-Archive: , List-Unsubscribe: , X-Spam-Score: -0.8 (/) Hi Toby, > Thanks for your thoughtful and encouraging comments, and for sharing some > of the libbitcoin implementation. Of course, you as well. > The architectural distinction I'd note is in composition. Libbitcoin isol= ates rules > as predicates but composes them inside phase-specific methods as if-chain= s. > This is excellent for a clean and readable node implementation. Hornet go= es > further and composes them in a static declarative graph using an algebra = of > combinators (All, With, Each). I wouldn't call this an architectural distinction given that it can be impl= emented over the set of rules in a matter of minutes. The design challenge = is in properly identifying and functionally isolating each rule. The block/= header/tx rules are the low hanging fruit. We implemented this well over 10= years ago, so I also don't know if I would consider it convergent: https://github.com/libbitcoin/libbitcoin-system/commit/4c6cd2874f5e0b490dc1= d7c020ace52858fb1b84#diff-d80e987b7f0628275c6e7318733e70848645f499b8a33c08f= 66d0f65b3f64e77R399 There are maybe two orders of magnitude more work in script evaluation alon= e (link to one part of it previously posted). And then there is at least de= serialization, storage, and chain organization - all while making this fit = architecturally into performance and public interface constraints. Providin= g meaningful formal verification across that space is a monumental task, wh= ich is why I'm encouraged that you are taking it on. But it does seem to me= that you may be underestimating it, even within Hornet's limited design ta= rget. > On widespread use: Hornet Node today is more of an experimental client fo= r > validation and IBD than a fully functional node. This is by design, as th= e main > target at this stage is the neutral specification This work can eventually produce a specification. The problem however will = remain faith in the correctness of the specification itself. Verification c= annot reasonably be applied to existing bitcoind implementations (and there= are a lot of them both in versions and in forks), and modifying them to th= e point where this is feasible becomes a new architecture (which is what we= have done). My prior comment on "widespread use" is about this specific pr= oblem. To solve this requires two things: (1) at least one fully consensus-verifiable node implementation. (2) the verified implementation(s) are predominant in economic use. Once this is the case, the rules become useful in the verification of other= implementations. > Some suggestions on collaboration might include: cross-validating libbitc= oin's > predicate set against Hornet's 34 semantic invariants to identify and res= olve > any divergence; joint review of the DSL as it develops; discussion on how= we > might verify that libbitcoin exactly implements the specification; and sh= aring a > corpus of edge-case test vectors. This all sounds reasonable. However, for us to invest limited resources it = requires that the outcome be meaningful. This small subset of the problem c= ould provide a proof of concept, which we could use to measure scope across= the entire surface. At that point we could balance further work on (1) abo= ve against also achieving (2). >> Are there any rules that you believe are missing >From my reading of rule names and descriptions here: https://github.com/tobysharp/hornet/blob/main/src/hornetlib/consensus/rules= /rules.h It appears that Hornet is missing the rule prohibiting forward references w= ithin a block. https://github.com/libbitcoin/libbitcoin-system/blob/master/src/chain/block= .cpp#L397-L417 This is a partial ordering constraint (is_forward_reference) that's easy to= miss because it's just a bitcoind implementation artifact. By isolating th= is behavior to its own rule, not only does it not get missed, but rule eval= uation also becomes order independent and therefore parallelizable. Otherwise there are potential malleation issues to deal with depending on h= ow blocks/headers are being managed. This can affect consensus behavior (vi= a archival) while not showing up as an issue in these rules. There is also = the rule prohibiting double spends, which can invalidate a context-free blo= ck (is_internal_double_spend), which would otherwise not be caught until co= ntextual checks (so is more of an optimization and malleation guard). https://github.com/libbitcoin/libbitcoin-system/blob/master/src/chain/block= .cpp#L422-L434 We avoid applying redundant rules except in the case of unconfirmed tx vali= dation, as it becomes necessary for DoS protection. But we label these as "= guards" not "rules". In this case the rules are block-level but must be eva= luated when accepting unconfirmed txs. The above is_internal_double_spend r= ule is a bit of an exception but it's context free, legitimately detects in= validity, precludes a type of malleation, and short-circuits a later more c= omprehensive/costly check. Best, Eric --=20 You received this message because you are subscribed to the Google Groups "= Bitcoin Development Mailing List" group. To unsubscribe from this group and stop receiving emails from it, send an e= mail to bitcoindev+unsubscribe@googlegroups.com. To view this discussion visit https://groups.google.com/d/msgid/bitcoindev/= 00b401dccf78%246f5e7a00%244e1b6e00%24%40voskuil.org.