JPYCv2 形式検証

外観

JPYC.setPermitNonce_permitNonces_ne ​

名称・種別 ​

  • 名称: JPYC.setPermitNonce_permitNonces_ne
  • 種別: theorem
  • モジュール: JpycFormalVerification.SignaturesTheorems
  • ソース: JpycFormalVerification/SignaturesTheorems.lean:66-68
  • 概要: setPermitNonce は当該 owner 以外の nonce を変えない、という補題。
  • 仕様: 対象外

型シグネチャ ​

lean
∀ (s : JPYC.State) (o a : JPYC.Address) (v : JPYC.U256), Ne a o → Eq ((s.setPermitNonce o v).permitNonces a) (s.permitNonces a)

o と異なるアドレス a については、setPermitNonce o v を施しても nonce が変わらない、という frame 補題です。

解説 ​

何を述べているか。 a ≠ o のとき (s.setPermitNonce o v).permitNonces a = s.permitNonces a です。1 点更新（Function.update）は更新キー以外を変えないので、Function.update_of_ne で従います。

直感。 「ある所有者の nonce を進めても、他人の nonce は一切動かない」を述べています。

なぜ安全性に効くか。 permit_nonce_frame（permit は所有者以外の nonce を変えない）の中核です。permit の効果が所有者 1 人に局所化されることを保証し、関係のないアカウントが巻き込まれないという フレーム性 を支えます。

図解 ​

Lean ソースコード ​

lean
theorem setPermitNonce_permitNonces_ne (s : State) (o a : Address) (v : U256) (h : a ≠ o) :
    (s.setPermitNonce o v).permitNonces a = s.permitNonces a := by
  simp [State.setPermitNonce, Function.update_of_ne h]

依存 ​