JPYCv2 形式検証

外観

JPYC.allowanceStep ​

名称・種別 ​

  • 名称: JPYC.allowanceStep
  • 種別: def
  • モジュール: JpycFormalVerification.ERC20
  • ソース: JpycFormalVerification/ERC20.lean:163-176
  • 概要: transferFrom の承認消費ステップ。無限承認は据え置き、有限なら value を引く。
  • 仕様: 対象外

型シグネチャ ​

lean
JPYC.State → JPYC.Address → JPYC.Address → JPYC.U256 → Except JPYC.Error JPYC.State

State・所有者 frm・支払い者 spender・金額 value を受け取り、transferFrom の許可額消費だけを行う補助関数です。許可額が MAX_U256 なら無限承認とみなし状態を変えず、そうでなければ value 以上あることを要求して value だけ減らします。

和訳 docstring ​

transferFrom の許可額消費ステップ ― 無限承認（type(uint256).max）は据え置き、有限なら value 分を要求して減算する。対応 Solidity: v2/FiatTokenV2.sol:248-252。

解説 ​

何を述べているか。 transferFrom の冒頭、allowance を消費するステップを切り出したものです。allowed[frm][spender] が MAX_U256（type(uint256).max）なら「無限承認」として 一切減らさず に通過。有限なら value ≤ 許可額 を要求し、checked な sub? で value だけ減らします。

直感。 「無限承認」は ERC20 で広く使われる慣習で、毎回の承認更新を省くためのものです。それを忠実に再現し、無限のときだけ許可額を据え置きます。

なぜ安全性に効くか。 allowance の扱いを 1 つの関数に集約することで、transferFrom の証明が「許可額ステップ」と「残高移動（_transfer）」に綺麗に分解できます。transferFrom_allowance（有限なら value 減・無限なら不変）と transferFrom_step_balances（このステップは残高・供給を動かさない）が、この分解に依存しています。

図解 ​

Lean ソースコード ​

lean
/-- The allowance-spending step of `transferFrom` — `v2/FiatTokenV2.sol:248-252`.

When `allowed[from][msg.sender] == type(uint256).max` the allowance is treated as
infinite and left untouched; otherwise it must cover `value` and is debited by it.
(The source caches `allowed[from][msg.sender]` in a local for gas; gas is out of
scope, so the read is inlined.) -/
def allowanceStep (s : State) (frm spender : Address) (value : U256) :
    Except Error State :=
  if s.allowed frm spender ≠ MAX_U256 then do
    req (value ≤ s.allowed frm spender) .transferExceedsAllowance
    let debited ← sub? (s.allowed frm spender) value
    pure (s.setAllowance frm spender debited)
  else
    pure s

対応 Solidity ソースコード ​

reference/JPYCv2/contracts/v2/FiatTokenV2.sol:248-252

solidity
// transferFrom 本体の冒頭（allowance を消費するステップ）
uint256 _allowed = allowed[from][msg.sender];
if (_allowed != type(uint256).max) {
    require(_allowed >= value, "FiatToken: transfer amount exceeds allowance");
    allowed[from][msg.sender] = _allowed - value;
}

依存 ​