From mboxrd@z Thu Jan 1 00:00:00 1970 Delivery-date: Sat, 18 Apr 2026 19:11:26 -0700 Received: from mail-oo1-f56.google.com ([209.85.161.56]) by mail.fairlystable.org with esmtps (TLS1.3) tls TLS_ECDHE_RSA_WITH_AES_128_GCM_SHA256 (Exim 4.94.2) (envelope-from ) id 1wEHd7-0001Lb-J0 for bitcoindev@gnusha.org; Sat, 18 Apr 2026 19:11:26 -0700 Received: by mail-oo1-f56.google.com with SMTP id 006d021491bc7-68e924f632bsf3388257eaf.0 for ; Sat, 18 Apr 2026 19:11:25 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1776564679; cv=pass; d=google.com; s=arc-20240605; b=Mxec4wv2ie3k9afkUUHhmV3bhk6eTaAYU/APG3oQiB128fwYxH/r8y0fzXyXpg4mDG 0Rz4Uts9TLI1U/kawuF7Tg0dNqHQnmqM7jH3HdUsSxm0WpO/5wwH1zrLPxN0cxYx71bE l7dF5WcBsJQDbsAXzVQTvQq/vPXKBGb9iGQUNojKGAxvF2/IhbU2iCOje4+xa3ltAhWh AA8b5OiYqF5UcCePCM2zXDe2pbze19RBKWyEd/awcibSQVk5o4kSe4yJqV3K51JTMBFA 7dOS5llTO/KTrJqzDPdXMc7a0pjwZ0FwnQ42QFvFMYsL6g46+BehTFaIMyq2U41N+R9H pM5Q== 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=mhgjNf26EyywavfvBW5k9yexo2PG/iHx+2Vpx9lP+II=; fh=Q/IFKrLqMJuSq3uU5LPfqj29vBlZH2l4PKoZn7x+4+8=; b=LsA8gXKY5U9zMK5MJLH7bgYUp1z2VQcCPu0HARpBltitxhFqocyzxudzBO5+MoASuA sEyBY5BKjs8QpvxesjB+lzSt0pyrhhaYG0V/KG9uFPPnNPWM0FaljaOWip9Uh7ONdyYB P0pYRpk2pEMh6nLbRiRK+SU8iCkKbjuhZC+is+cYyOXhv/7c6AXk6mywh0/4i3xNwLQL Xq9T6zvcB9QbYcQ3mWh+ysJ5cPMa27DP98l+dAQd6O/1dXyC73cR8H+KYUFjGpZx8rmi vOm614jm13X1/9+YxbKP1cbJUcTqH5UAjCKcv3pznI605+yQgvZTVCTla8Ab/b8SGlxj REBA==; darn=gnusha.org ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@voskuil.org header.s=google header.b=evnwqtn3; spf=pass (google.com: domain of eric@voskuil.org designates 2607:f8b0:4864:20::f30 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=1776564679; x=1777169479; 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=mhgjNf26EyywavfvBW5k9yexo2PG/iHx+2Vpx9lP+II=; b=R9/kt83WIO2Db7prIxwUN0GhukyScA+aD35GzE+XsI0b2IjKd48Ib/o0uARGXjGQ+p zAk0Pqbm41krRHwIO+nbcagFXdEBrMbASN9b8AlXcmh4cBqoQ2Xx9I9YhalC8d0cZRip etP4/ECBRKBqL60/HhfOMI9lA3jp82MwXLU4HlsZGJZ1oOgwFs+7Uv1v5OqFLnik3Bap uBhchWAgjt1MbZfMeB3odvR6fzG49+ufJRWCh6PMzBaPSrn0lbzrSCQdS24enYVq7RmT GGg7JecktKUt9/hByULUcVXmE5hv8DuNR5TJV93c0ztrBdB0ByKSXj2NN8WFwRyg6UMO LvIg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20251104; t=1776564679; x=1777169479; 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=mhgjNf26EyywavfvBW5k9yexo2PG/iHx+2Vpx9lP+II=; b=kVpj33Nd27hmAjOyLOuE1M/D7nF7P5j4t+KqU+BSM929g3u/rWEh3YAyhv9O9R0Qhz tSTu4qzwjU7GvAa/3DmZNVUIZj62SmYhSwSmh/9aHG35daDuuThVpzL7vN+AqPk0gVN3 iXoepGXzK04Ap0q5S3Hn1oji9EO6KNoSwIGdvINExAKrc7SO2B+4KGhRkml1Mip6m3kV naghHbleFH4rmZbAaAStvM91t3iOB61wqCDquqVYK1zH9BjCREBtb0xFVRF6QATwaOa8 YGJ3i0WpOv63yrJdezzFHtnIK5C4/PIRg94duyebIukSyAc1Lz0+B5TlRLunDv2rERmq ZY3w== Sender: bitcoindev@googlegroups.com X-Forwarded-Encrypted: i=2; AFNElJ+BBHEtIj/GgzwEJxZt8/i0NfE27p6h8ThBytySk9XKfToLN272SJ4etTZZhfJgxJBtdQGBQ83t2nOL@gnusha.org X-Gm-Message-State: AOJu0Yzx1F8cpfE9khqGqB0mkUJgBdXxt+wsEKvlUdUQFgNS3+b+aL+G xJ6XRRNZx/64wrsGWxn2TvwaOnhlYRd2f2DTdHdVEHxl0ldZ1UzviAGW X-Received: by 2002:a05:6820:1b15:b0:684:9e9e:816c with SMTP id 006d021491bc7-69462f2041cmr5113277eaf.41.1776564679192; Sat, 18 Apr 2026 19:11:19 -0700 (PDT) X-BeenThere: bitcoindev@googlegroups.com; h="AYAyTiJtwTCkLZ0fyfqBb/eKFVtL+4kZ8tlFwdnvXhp/uRQxkw==" Received: by 2002:a05:6871:295:b0:417:5927:12e9 with SMTP id 586e51a60fabf-4280c660f3dls1878500fac.2.-pod-prod-01-us; Sat, 18 Apr 2026 19:11:14 -0700 (PDT) X-Forwarded-Encrypted: i=2; AFNElJ/OZygczQDj6hUumJ3nO08aXkWwkpQG0yMBveE6w6RAyIVDcA6Fm+dvYHv3JEddP6NwLv4a/cbkRIGm@googlegroups.com X-Received: by 2002:a05:6808:4f29:b0:467:100d:22ba with SMTP id 5614622812f47-4799c8f274emr4502311b6e.18.1776564674034; Sat, 18 Apr 2026 19:11:14 -0700 (PDT) Received: by 2002:a05:6808:1d1e:b0:479:8e15:9311 with SMTP id 5614622812f47-4799c9889b1msb6e; Sat, 18 Apr 2026 19:07:45 -0700 (PDT) X-Forwarded-Encrypted: i=2; AFNElJ/G206BAGqz6OSMH+xKDdNU8mXhIDNA8aPX/dg9SdyxDJObeAuTj8PQWKMXesy+Yl4EuKlE2gOmL4MI@googlegroups.com X-Received: by 2002:a4a:e914:0:b0:683:8361:8be5 with SMTP id 006d021491bc7-69462ef0ee5mr4445521eaf.35.1776564465404; Sat, 18 Apr 2026 19:07:45 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1776564465; cv=none; d=google.com; s=arc-20240605; b=GHQh9td+ie9flJ0++x6c8d8D/INamYQ7zaK0HWvLA2fdw/XA4z0Mf1lU6gIh9ZD1ii xxT8P7TSqr7W8xDSVJWa+zQcZb2c0tR1RJiETkV+fGi+ZDm4QMRoSr8Hc99Uct5zlovL 1r9aszgsFzgqsEO2s77mHP0ydhdXT2XZ/+4LdVCXFpkJi3m9sh6H+AQvuYDsE4q4JO0j bBC4TiNVMdddz5C9TNfI+KPv57B5gZDUN6sudFWnvnwBYxJaZ5sIkd9iD57kZspv8mR9 K3xPJq45JZgjD0IksEsW2tqjEUO7TISdl0hZ7+qDThOIcBB00UH8MgdIvGgYksQnfQAA e2Kg== 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=c7ou1c6LkG8kjhc6JDfYLHy1KHr+sBy1rWC1VT+N5t0=; fh=mpvKJ+kveXoCCb8tw+uwxoTvx9KW895otpu26+S5ffo=; b=VDr8oCkiyYUc1O+hTwbZr2iWcjCukRqkZ3QidGmbPMOdG0wWxXiHYjMjmep/QqTCf2 3+JK/iPRZl36q0M2WkYkik4bwG8xLR2ASFG3JiQTqBt902spwScde8YUvYXD/Ei9HWk8 yqCoeweNCX4rZXzcL+05eE2GodZ8Z09xrnys0dJqSEaW4HSpapqhLfUFmdZNCEw5s+yM 6rD/M3rMT7n4pkAOWUZcftTNLLNf6bI1zZaBaLEmk1vHYdXoKzEgyw4wMgFqyhzmll0y 7HtfAmCeEpzm9/inJEVuqsC/jIZB9H/4PEdlqKsxu5lCI89nES5RDIOH1Xcmjkkz/9mQ TR+g==; dara=google.com ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@voskuil.org header.s=google header.b=evnwqtn3; spf=pass (google.com: domain of eric@voskuil.org designates 2607:f8b0:4864:20::f30 as permitted sender) smtp.mailfrom=eric@voskuil.org; dara=pass header.i=@googlegroups.com Received: from mail-qv1-xf30.google.com (mail-qv1-xf30.google.com. [2607:f8b0:4864:20::f30]) by gmr-mx.google.com with ESMTPS id 006d021491bc7-69464f8e560si219804eaf.3.2026.04.18.19.07.45 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Sat, 18 Apr 2026 19:07:45 -0700 (PDT) Received-SPF: pass (google.com: domain of eric@voskuil.org designates 2607:f8b0:4864:20::f30 as permitted sender) client-ip=2607:f8b0:4864:20::f30; Received: by mail-qv1-xf30.google.com with SMTP id 6a1803df08f44-89fc4147f2eso22446686d6.3 for ; Sat, 18 Apr 2026 19:07:45 -0700 (PDT) X-Forwarded-Encrypted: i=1; AFNElJ/fIyNljnZco9Sb9Hnar0ROb5ItKRHiusjrUOtclsSgCIkBR2xMHL0EOESv2CpLjqxvNUfA5q9cys6I@googlegroups.com X-Gm-Gg: AeBDievLPGtj8ntpxqerbrW6bQDVa8MbyjKPNjikAs18bUYA2YIB/1FW7KH6JUpR9XK vaktxPAW1XvkpGnSsiG122BT2OE15YyqiG5yWktHcX81BaadUaWFW8XpFOecbyRZRo0lCfVtXT5 MzUBYt/gvz49Pj2ZukE0hY2AGmRMRMuVosf15bSHoVV2xjwEAeJWsv7dEL06KN8ZN8rTqoHQtmE oomAxuX7yDmGiEtW/lYaZRtNnYO/aVrfwjTMW9SRo1EMSavVwWvJrLzFdNYpl5k2JhM+Oncdb7K ESJ0jDX62XRCjV53VeqBHw4KUDbWo0N5yTxCJl/HE54nu/dh1hPVVNDfGIxUHwVyyYREANJp7QK SyO1s2L4KN5vwyScM5CHMzy7jRxkbhpufCPHLVNIvBMqdM/Tab3VlR4/qFTIQVwncqFeQ4r1qMy O8pJbX7JwbZws5w9UJo8AwOvSyPF0BXsxJu5dsaGL+17eWo/lwFo3PriOup6J+jZ+Qo9I1muee1 Kir X-Received: by 2002:ad4:5ae4:0:b0:8ac:b542:1063 with SMTP id 6a1803df08f44-8b0280474bemr149112166d6.15.1776564464276; Sat, 18 Apr 2026 19:07:44 -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-8b02ae86947sm59661886d6.37.2026.04.18.19.07.43 (version=TLS1_2 cipher=ECDHE-ECDSA-AES128-GCM-SHA256 bits=128/128); Sat, 18 Apr 2026 19:07:43 -0700 (PDT) From: To: "'Toby Sharp'" , "'Bitcoin Development Mailing List'" References: <4cd864f3-96dd-4058-bfcd-b1bbf6cfa269n@googlegroups.com> <006501dccd36$ea035fd0$be0a1f70$@voskuil.org> <00b401dccf78$6f5e7a00$4e1b6e00$@voskuil.org> <--C53DoYZLFJgwz6T6jBLFNjx3dNCZRC06RK981Cj40XsyFGNMf2pX7eiUpG-hzsMXnEIxFFyEWjost7GyuM3xKkvpqj99ODyTQprnl-N1g=@hornetnode.org> In-Reply-To: <--C53DoYZLFJgwz6T6jBLFNjx3dNCZRC06RK981Cj40XsyFGNMf2pX7eiUpG-hzsMXnEIxFFyEWjost7GyuM3xKkvpqj99ODyTQprnl-N1g=@hornetnode.org> Subject: RE: RE: [bitcoindev] Hornet Update: A declarative executable specification of Bitcoin consensus rules Date: Sat, 18 Apr 2026 22:07:42 -0400 Message-ID: <000d01dccfa1$4e927e60$ebb77b20$@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: AQIM7pKi29ODGLwkBcXlBApwgU5LuwFCflclAfG4G9gCVCp9VAIp4ByotUfRdxA= 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=evnwqtn3; spf=pass (google.com: domain of eric@voskuil.org designates 2607:f8b0:4864:20::f30 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 (/) > > It appears that Hornet is missing the rule prohibiting forward referenc= es > within a block. >=20 > This is implied by Rule S02: "A transaction input MUST reference a previo= us > transaction output that remains unspent." However, to make it clearer, I = will > rewrite it as: >=20 > "S02: A transaction input MUST reference a preceding transaction output t= hat > remains unspent." As I understand it, the rule in question: // Returns success if every spending input in this block references an ex= isting unspent output. consensus::Result QueryPrevoutsUnspent(const protocol::Block& block) cons= t override { Assert(&block =3D=3D joiner_->GetBlock().get()); if (!joiner_->WaitForQuery()) return consensus::Error::Spending_Prevout= NotUnspent; return {}; } =20 can only fail if the query fails, and the query itself is not subject to ve= rification. In this case the consensus rule is implemented as a side effect= of the query (as it is in bitcoind), and the query itself is not subject t= o verification. I would consider this a missing rule from the perspective o= f verification. It is true that the store must provide fidelity in any case= (what goes in must come out). That alone presents significant issues for v= erification. But at least it's straightforward to define. But in this case = the query is not just returning outputs that have been stored in the block = total ordering. The query is constructing a temporary map, accumulating block-internal spen= ds into that map in a specific order, populating the results, and effective= ly enforcing the forward reference constraint as side effect of the populat= ion implementation. These outputs are not placed into the utxo store until = after the block is validated. In other words, the consensus rule is evaluat= ed entirely within the scope of the query; it is not a consequence of simpl= e store fidelity, and is not a consequence of a verified rule. It's lurking= in an unverified query. If another implementation was to populate prevouts= differently (e.g., in parallel), and with full fidelity, the ordering cons= traint easily disappears and is not caught by verification. This has happen= ed, and IIRC resulted in the loss of a block by a miner. This is the type o= f consensus break that verification presumes to preclude. > > Otherwise there are potential malleation issues to deal with depending = on > how blocks/headers are being managed. This can affect consensus behavior > (via archival) while not showing up as an issue in these rules. >=20 > That would be an implementation correctness detail rather than part of a > declarative spec. >=20 > The intention here is to specify what must be true for consensus validity= rather > than how it should be computed. The whole point is verifying implementation correctness. Calling it out of = scope doesn't really solve the problem. Merkle root malleation has resulted= in consensus failure (bitcoin core). Transaction deserialization has resul= ted in consensus failure (btcd). Store infidelity has resulted in consensus= failure (bitcoind). Cryptographic library bugs have produced consensus bug= s that were preemptively patched (openssl). These types of issues are more = common in modern history than what one might consider "rules". The so-calle= d rules are actually much easier to deal with. Airing out some of these real difficulties has been worthwhile. In my exper= ience people have an overly optimistic view of what can be achieved by both= formal verification and the attempt to create a shared script implementati= on. I'm hopeful, but I also try to stay grounded. I'll give further respons= es offline. Best, Eric https://nvd.nist.gov/vuln/detail/CVE-2022-39389 https://nvd.nist.gov/vuln/detail/CVE-2012-2459 https://nvd.nist.gov/vuln/detail/CVE-2013-3220 --=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/= 000d01dccfa1%244e927e60%24ebb77b20%24%40voskuil.org.