JPYC.CallContext

名称・種別

• 名称: JPYC.CallContext
• 種別: structure
• モジュール: JpycFormalVerification.Address
• ソース: JpycFormalVerification/Address.lean:20-35
• 概要: モデルが依存する msg.sender・block.timestamp・block.chainid をまとめた呼び出し文脈。
• 仕様: 対象外

型シグネチャ

Type

Type ＝ いくつかのフィールドを束ねた 構造体 を定義します。sender（msg.sender）と、既定値 0 の blockTimestamp（block.timestamp）・blockChainId（block.chainid）の 3 フィールドを持ちます。

和訳 docstring

関数モデルが依存する EVM メッセージフレームの一部。

sender は msg.sender。blockTimestamp / blockChainId は block.timestamp / block.chainid で、EIP-2612（permit の期限）と EIP-3009（validAfter / validBefore、および _domainSeparatorV4 のキャッシュ済みか再計算かの分岐）で使う。ブロック関連フィールドは既定値 0。これにより、これらを読まない Phase 0–2 の関数は { sender := … } だけで文脈を構築でき、それらのフェーズでは値は無関係。

解説

何を述べているか。「誰が・いつ・どのチェーンで」呼び出したかをまとめた構造体です（primer §3.5）。

直感。 Solidity では msg.sender などは暗黙のグローバル変数ですが、Lean のモデル関数は純粋（引数だけで結果が決まる）なので、呼び出しの文脈を明示的に引数として渡します。権限チェック（msg.sender == owner など）や署名の有効期限判定の入力になります。

なぜ安全性に効くか。 権限・有効期限といったセキュリティ上の判断材料を 1 か所に固め、どの関数がどの文脈情報に依存するかを型レベルで可視化します。blockTimestamp / blockChainId を既定値 0 にしてあるのは後方互換のための工夫で、これらを読まないフェーズの安全性証明には影響しません。

図解

Lean ソースコード

/-- The portion of the EVM message frame the functional model depends on.

`sender` is `msg.sender`; `blockTimestamp` / `blockChainId` are `block.timestamp`
/ `block.chainid`, consumed by EIP-2612 (`permit` deadline) and EIP-3009
(`validAfter` / `validBefore`, and the cached-vs-recomputed domain-separator
branch in `_domainSeparatorV4`). The block fields default to `0` so that the
Phase 0–2 functions — which never read them — can keep constructing a context
from just `{ sender := … }`; their values are immaterial to those phases. -/
structure CallContext where
  /-- `msg.sender`. -/
  sender : Address
  /-- `block.timestamp` (unix time). -/
  blockTimestamp : U256 := 0
  /-- `block.chainid`. -/
  blockChainId : U256 := 0
  deriving DecidableEq, Repr

依存

（なし）