JPYC.sub?

名称・種別

• 名称: JPYC.sub?
• 種別: def
• モジュール: JpycFormalVerification.Word
• ソース: JpycFormalVerification/Word.lean:40-43
• 概要: Solidity 0.8 のチェック付き減算。b > a なら revert する。
• 仕様: 対象外

型シグネチャ

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

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

和訳 docstring

Solidity 0.8 の checked 減算。b > a の場合に限り、Panic(0x11)（Error.arithmeticUnderflow としてモデル化）で revert する。

解説

何を述べているか。 あふれを検知する引き算です（primer §3.4）。b.toNat ≤ a.toNat なら .ok (a - b)、b > a なら .error arithmeticUnderflow を返します。

直感。 結果がマイナスになる引き算は revert します。符号なし整数ではマイナスを表せないからです。

なぜ安全性に効くか。 残高から差し引く操作はこの演算を通すので、残高がマイナス（= 巨大な値へラップ）に壊れることがありません。「残高から value を引けた」という事実から「value ≤ 残高」が導けること（sub?_eq_ok）が、二重支払い・残高破壊を防ぐ鍵になります。

図解

Lean ソースコード

/-- Solidity 0.8 checked subtraction. Reverts with `Panic(0x11)` (modeled as
`Error.arithmeticUnderflow`) iff `b > a`. -/
def sub? (a b : U256) : Except Error U256 :=
  if b.toNat ≤ a.toNat then .ok (a - b) else .error .arithmeticUnderflow

依存

• JPYC.Error
• JPYC.U256