論文の概要: Hornet Node and the Hornet DSL: A Minimal, Executable Specification for Bitcoin Consensus

• arxiv url: http://arxiv.org/abs/2509.15754v1
• Date: Fri, 19 Sep 2025 08:30:27 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-22 18:18:11.080297
• Title: Hornet Node and the Hornet DSL: A Minimal, Executable Specification for Bitcoin Consensus
• Title（参考訳）: Hornet NodeとHornet DSL:Bitcoin合意のための最小限の実行可能な仕様
• Authors: Toby Sharp,
• Abstract要約: 我々は、メインネットを数時間でチップにシンクするBitcoinコンセンサスルールのC++仕様を1スレッドで提示する。 また、これらのルールをあいまいにコード化するように設計されたHornet Domain-Specific Language(Hornet DSL)を紹介します。 私たちは、Hornet NodeとHornet DSLが、Bitcoinコンセンサスの純粋で形式的で実行可能な仕様への最初の信頼できるパスを提供する、と論じています。
• 参考スコア（独自算出の注目度）: 0.38073142980733005
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Bitcoin's consensus rules are encoded in the implementation of its reference client: "The code is the spec." Yet this code is unsuitable for formal verification due to side effects, mutable state, concurrency, and legacy design. A standalone formal specification would enable verification both across versions of the reference client and against new client implementations, strengthening decentralization by reducing the risk of consensus-splitting bugs. Yet such a specification has long been considered intractable given the complexity of Bitcoin's consensus logic. We demonstrate a compact, executable, declarative C++ specification of Bitcoin consensus rules that syncs mainnet to tip in a few hours on a single thread. We also introduce the Hornet Domain-Specific Language (DSL) specifically designed to encode these rules unambiguously for execution, enabling formal reasoning, consensus code generation, and AI-driven adversarial testing. Our spec-driven client Hornet Node offers a modern and modular complement to the reference client. Its clear, idiomatic style makes it suitable for education, while its performance makes it ideal for experimentation. We highlight architectural contributions such as its layered design, efficient data structures, and strong separation of concerns, supported by production-quality code examples. We argue that Hornet Node and Hornet DSL together provide the first credible path toward a pure, formal, executable specification of Bitcoin consensus.
• Abstract（参考訳）: Bitcoinのコンセンサスルールはリファレンスクライアントの実装にエンコードされている。 しかし、このコードは副作用、変更可能な状態、並行性、レガシー設計のために正式な検証には適していない。 スタンドアロンの形式仕様は、参照クライアントのバージョンと新しいクライアント実装の両方に対する検証を可能にし、コンセンサス分離バグのリスクを減らすことで分散化を強化する。 しかし、Bitcoinのコンセンサスロジックの複雑さを考えると、そのような仕様は長い間、難解であると考えられてきた。 我々は、1スレッドでメインネットを数時間でチップにシンクするBitcoinコンセンサスルールのコンパクトで実行可能な宣言型C++仕様を実証する。 また、Hornet Domain-Specific Language(DSL)を導入し、これらのルールをあいまいにコード化し、形式的推論、コンセンサスコード生成、AI駆動の対向テストを可能にします。 仕様駆動のクライアントであるHornet Nodeは、リファレンスクライアントのモダンでモジュール化された補完を提供します。 その明瞭で慣用的なスタイルは教育に適しており、そのパフォーマンスは実験に最適である。 私たちは、その階層設計、効率的なデータ構造、製品品質のコード例でサポートされている強い関心の分離といったアーキテクチャ上の貢献を強調します。 私たちは、Hornet NodeとHornet DSLが、Bitcoinコンセンサスの純粋で形式的で実行可能な仕様への最初の信頼できるパスを提供する、と論じています。

関連論文リスト

• Decompiling Smart Contracts with a Large Language Model [51.49197239479266]
  Etherscanの78,047,845のスマートコントラクトがデプロイされているにも関わらず(2025年5月26日現在)、わずか767,520 (1%)がオープンソースである。 この不透明さは、オンチェーンスマートコントラクトバイトコードの自動意味解析を必要とする。 バイトコードを可読でセマンティックに忠実なSolidityコードに変換する,先駆的な逆コンパイルパイプラインを導入する。
  論文  参考訳（メタデータ） (2025-06-24T13:42:59Z)
• GRIFFIN: Effective Token Alignment for Faster Speculative Decoding [52.905060461479856]
  GRIFFINは、トークン指向のトレーニング戦略とトークン指向のドラフトモデルを組み込んだ、新しいフレームワークである。 LLaMA, Vicuna, Qwen, Mixtral モデルを用いた実験では, GRIFFIN が平均受容長 8% 以上, スピードアップ比 7% 以上を達成している。
  論文  参考訳（メタデータ） (2025-02-16T07:06:00Z)
• Formal Model Guided Conformance Testing for Blockchains [1.4838910416636741]
  本稿では,プロトコルの形式モデルを用いたプロトコル適合性テストを行うフレームワークを提案する。 私たちのフレームワークは、トレースジェネレータとチェッカーとしてコンポーネントを使用する2つの補完的なコンポーネントで構成されています。
  論文  参考訳（メタデータ） (2025-01-15T03:20:13Z)
• Validated Strong Consensus Protocol for Asynchronous Vote-based Blockchains [4.79997217554732]
  投票ベースのブロックチェーンは、Byzantine Fault Toleranceコンセンサスプロトコルを使用して、ある状態から別の状態へ移行する。 本稿では,非同期環境におけるリーダベースの協調を可能にする,強大なBFTコンセンサスモデルを提案する。 我々のプロトコルはメッセージの複雑さを大幅に減らし、しきい値のシグネチャに頼ることなく線形ビューの変更を実現する最初のプロトコルです。
  論文  参考訳（メタデータ） (2024-09-12T15:54:40Z)
• Secure compilation of rich smart contracts on poor UTXO blockchains [0.8192907805418581]
  UTXOモデルのための中間レベル言語であるILLUMを提案する。 コンパイラをILLUMから、ループフリースクリプトでベアボーンのUTXOブロックチェーンに定義する。 コベナント(covenants)は、トランザクションのチェーンに沿ってスクリプトを保存するメカニズムです。
  論文  参考訳（メタデータ） (2023-05-16T15:40:18Z)
• ReCode: Robustness Evaluation of Code Generation Models [90.10436771217243]
  コード生成モデルのための総合的ロバストネス評価ベンチマークであるReCodeを提案する。 ドクストリング、関数と変数名、コード構文、コードフォーマットのコードに特化して、30以上の変換をカスタマイズします。 ヒトのアノテータでは、摂動プロンプトの90%以上が本来のプロンプトの意味を変えていないことが確認された。
  論文  参考訳（メタデータ） (2022-12-20T14:11:31Z)
• Speculative Decoding: Exploiting Speculative Execution for Accelerating Seq2seq Generation [80.2267931231335]
  本稿では,自己回帰(AR)デコーディングを高速化する投機的実行のアイデアを活用するための投機的デコーディング(SpecDec)を提案する。 SpecDecには2つのイノベーションがある。Spec-Drafter - 効率的なドラフトのために特別に最適化された独立モデル、Spec-Verification - ドラフトされたトークンを効率的に検証するための信頼性の高い方法である。
  論文  参考訳（メタデータ） (2022-03-30T17:27:09Z)
• Quantum Multi-Solution Bernoulli Search with Applications to Bitcoin's Post-Quantum Security [67.06003361150228]
  作業の証明(英: proof of work、PoW)は、当事者が計算タスクの解決にいくらかの労力を費やしたことを他人に納得させることができる重要な暗号構造である。 本研究では、量子戦略に対してそのようなPoWの連鎖を見つけることの難しさについて検討する。 我々は、PoWs問題の連鎖が、マルチソリューションBernoulliサーチと呼ばれる問題に還元されることを証明し、量子クエリの複雑さを確立する。
  論文  参考訳（メタデータ） (2020-12-30T18:03:56Z)
• Deep Just-In-Time Inconsistency Detection Between Comments and Source Code [51.00904399653609]
  本稿では,コード本体の変更によりコメントが矛盾するかどうかを検出することを目的とする。 私たちは、コメントとコードの変更を関連付けるディープラーニングアプローチを開発しています。 より包括的な自動コメント更新システムを構築するために,コメント更新モデルと組み合わせて提案手法の有用性を示す。
  論文  参考訳（メタデータ） (2020-10-04T16:49:28Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。