JPYCv2 形式検証

外観

JPYC.WF_setAuthorizationState ​

名称・種別 ​

  • 名称: JPYC.WF_setAuthorizationState
  • 種別: theorem
  • モジュール: JpycFormalVerification.SignaturesTheorems
  • ソース: JpycFormalVerification/SignaturesTheorems.lean:92-99
  • 概要: 0/1 を書く限り setAuthorizationState は WF を保つ、という補題。
  • 仕様: 対象外

型シグネチャ ​

lean
∀ {s : JPYC.State}, JPYC.WF s → ∀ (a : JPYC.Address) (n : JPYC.Bytes32) {v : JPYC.U256}, Or (Eq v 0) (Eq v 1) → JPYC.WF (s.setAuthorizationState a n v)

事前状態が WF を満たし、authorization 台帳に 0 または 1 を書き込むなら、書き込み後も WF が保たれる、という補題です。

和訳 docstring ​

setAuthorizationState が 0/1 を書く限り authorizationStates の 0/1 性は保たれ、他の WF フィールドは不変。

解説 ​

何を述べているか。 State.setAuthorizationState は (authorizer, nonce) の 1 マスに値 v を書きます。v が 0 か 1 のいずれかなら、「authorizationStates は 0/1 値」という WF の条件は崩れません。他の WF 条件（ブロック・許可リストフラグ・initializedVersion）は触れていないのでそのまま保たれます。

直感。 「authorization のマスには 0 か 1 しか書かない」というモデルの約束を、WF 保存の形で確認します。証明は共通補助 binaryFlag_update₂ に委ね、更新マスは v ∈ {0,1}、それ以外は元の WF を使います。

なぜ安全性に効くか。 transferWithAuthorization_wf / receiveWithAuthorization_wf / cancelAuthorization_wf の土台です。署名操作が WF を壊さないことを保証し、フラグに依存する判定ロジックの前提を守ります。

図解 ​

Lean ソースコード ​

lean
/-- `setAuthorizationState` keeps `authorizationStates` 0/1-valued when it writes a
0/1; the other `WF` fields are untouched. -/
theorem WF_setAuthorizationState {s : State} (hwf : WF s) (a : Address) (n : Bytes32) {v : U256}
    (hv : v = 0 ∨ v = 1) : WF (s.setAuthorizationState a n v) where
  blocklistedBinary := hwf.blocklistedBinary
  allowlistedBinary := hwf.allowlistedBinary
  authStateBinary := binaryFlag_update₂ hwf.authStateBinary a n hv
  initializedVersionValid := hwf.initializedVersionValid

依存 ​