JPYCv2 形式検証

外観

JPYC.add? ​

名称・種別 ​

  • 名称: JPYC.add?
  • 種別: def
  • モジュール: JpycFormalVerification.Word
  • ソース: JpycFormalVerification/Word.lean:35-38
  • 概要: Solidity 0.8 のチェック付き加算。和が 256 ビットに収まらなければ revert する。
  • 仕様: 対象外

型シグネチャ ​

lean
JPYC.U256 → JPYC.U256 → Except JPYC.Error JPYC.U256

U256 → U256 → Except Error U256：2 つの U256 を受け取り、成功（和）か失敗（オーバーフロー）か を返します。

和訳 docstring ​

Solidity 0.8 の checked 加算。正確な和が 256 ビットに収まらない場合に限り、Panic(0x11)（Error.arithmeticOverflow としてモデル化）で revert する。

解説 ​

何を述べているか。 あふれを検知する足し算です（primer §3.4）。a.toNat + b.toNat < 2^256 なら .ok (a + b)、そうでなければ .error arithmeticOverflow を返します。

直感。 Solidity 0.8 以降は加算がオーバーフローすると自動で revert します。その挙動を忠実に再現しています。

なぜ安全性に効くか。 残高・供給・許可額の加算は必ずこの演算を通すので、ラップアラウンド（桁あふれで小さな値に戻る現象）で数字が壊れることがありません。成功時には自然数の和と一致すること（add?_toNat）も別途証明されています。

図解 ​

Lean ソースコード ​

lean
/-- Solidity 0.8 checked addition. Reverts with `Panic(0x11)` (modeled as
`Error.arithmeticOverflow`) iff the exact sum does not fit in 256 bits. -/
def add? (a b : U256) : Except Error U256 :=
  if a.toNat + b.toNat < 2 ^ 256 then .ok (a + b) else .error .arithmeticOverflow

依存 ​