JPYCv2 形式検証

外観

JPYC.transferResult ​

名称・種別 ​

  • 名称: JPYC.transferResult
  • 種別: def
  • モジュール: JpycFormalVerification.ERC20Theorems
  • ソース: JpycFormalVerification/ERC20Theorems.lean:124-128
  • 概要: 成功した _transfer の結果状態：frm を value だけ引き、引いた後の状態から dst に足す。
  • 仕様: 対象外

型シグネチャ ​

lean
JPYC.State → JPYC.Address → JPYC.Address → JPYC.U256 → JPYC.U256 → JPYC.State

State・frm・dst・value・credited を受け取り、_transfer が成功したときの結果状態 ―「frm を value 減らし、続けて dst を credited にした状態」― を表す関数です。

和訳 docstring ​

成功した _transfer が生む「減算後に加算した」結果状態 ― frm を value 減らし、更新後の状態から dst を再読み込みして加算する。

解説 ​

何を述べているか。 成功した内部送金 _transfer が作る状態を、명示的な式として与えます。まず frm の残高を balances frm - value に下げ（setBalance）、その 更新後 の状態で dst を credited に設定します。

直感。 送金は「引いてから足す」の 2 段更新です。dst の加算は frm を引いた後の状態を見るため、frm == dst（自己送金）のときは引いた分が足し戻され、結果として無変化になります。

なぜ安全性に効くか。 _transfer の結果をこの形に正規化することで、フレーム性・局所/大域の供給保存・自己送金安全性の計算が、Function.update の代数的補題だけで進められます。各 transfer_* 定理が共通して参照する「結果の形」です。

図解 ​

Lean ソースコード ​

lean
/-- The debited-then-credited state produced by a successful `_transfer`: the
payer `frm` is debited `value`, then `dst` is credited (re-reading its balance
from the already-debited state). -/
def transferResult (s : State) (frm dst : Address) (value credited : U256) : State :=
  (s.setBalance frm (s.balances frm - value)).setBalance dst credited

依存 ​