JPYCv2 形式検証

外観

JPYC.setAuthorizationState_self ​

名称・種別 ​

  • 名称: JPYC.setAuthorizationState_self
  • 種別: theorem
  • モジュール: JpycFormalVerification.SignaturesTheorems
  • ソース: JpycFormalVerification/SignaturesTheorems.lean:87-89
  • 概要: setAuthorizationState 後、当該 (authorizer,nonce) の状態が設定値になる、という補題。
  • 仕様: 対象外

型シグネチャ ​

lean
∀ (s : JPYC.State) (a : JPYC.Address) (n : JPYC.Bytes32) (v : JPYC.U256), Eq ((s.setAuthorizationState a n v).authorizationStates a n) v

authorization を使用済みに設定した直後に同じ鍵で読み出すと、設定した値 v がそのまま返る、という @[simp] 等式です。

解説 ​

何を述べているか。 (s.setAuthorizationState a n v).authorizationStates a n = v を示します。authorization を使用済みに設定で書いた値が、同じ鍵での読み出しでそのまま得られます（Function.update_self）。

直感。 「書いた値はそのまま読める」という当たり前を、機械が自動で使える形（@[simp]）で確認しています。

なぜ安全性に効くか。 効果系の定理（transferWithAuthorization_marks_used など）が「設定した値が実際に反映される」と結論づけるための核心の補題です。

図解 ​

Lean ソースコード ​

lean
@[simp] theorem setAuthorizationState_self (s : State) (a : Address) (n : Bytes32) (v : U256) :
    (s.setAuthorizationState a n v).authorizationStates a n = v := by
  simp [State.setAuthorizationState, Function.update_self]

依存 ​