全宣言一覧（392 宣言）

カテゴリー すべてAccessControlFoundationERC20SignaturesUpgradeability 種別 すべてdeftheoremabbrevstructureinductiveinstance 仕様=対象 のみ 405 / 405 件（仕様=対象 219 件）

名前	種別	カテゴリー	モジュール	概要	仕様	依存数
State.setTotalSupply	def	AccessControl	AccessControl.lean	totalSupply_ を v に書き換える純粋な状態更新関数。	対象外	2
State.setMinterAllowed	def	AccessControl	AccessControl.lean	minterAllowed[a] を v に書き換える純粋な状態更新関数。	対象外	3
State.setMinter	def	AccessControl	AccessControl.lean	minters[a] を b に書き換える純粋な状態更新関数。	対象外	2
State.setOwner	def	AccessControl	AccessControl.lean	_owner を a に書き換える更新関数（Ownable._transferOwnership）。	対象外	2
State.setPauser	def	AccessControl	AccessControl.lean	pauser を a に書き換える純粋な状態更新関数。	対象外	2
State.setBlocklister	def	AccessControl	AccessControl.lean	blocklister を a に書き換える純粋な状態更新関数。	対象外	2
State.setMinterAdmin	def	AccessControl	AccessControl.lean	minterAdmin を a に書き換える純粋な状態更新関数。	対象外	2
State.setAllowlister	def	AccessControl	AccessControl.lean	allowlister を a に書き換える純粋な状態更新関数。	対象外	2
State.setPaused	def	AccessControl	AccessControl.lean	paused フラグを b に書き換える純粋な状態更新関数。	対象外	1
State.setBlocklisted	def	AccessControl	AccessControl.lean	blocklisted[a] を v に書き換える純粋な状態更新関数。	対象外	3
State.setAllowlisted	def	AccessControl	AccessControl.lean	allowlisted[a] を v に書き換える純粋な状態更新関数。	対象外	3
onlyOwner	def	AccessControl	AccessControl.lean	onlyOwner 修飾子。owner() ≠ msg.sender なら revert する権限ガード。	対象外	5
onlyPauser	def	AccessControl	AccessControl.lean	onlyPauser 修飾子。msg.sender ≠ pauser なら revert する権限ガード。	対象外	5
onlyBlocklister	def	AccessControl	AccessControl.lean	onlyBlocklister 修飾子。msg.sender ≠ blocklister なら revert する権限ガード。	対象外	5
onlyMinters	def	AccessControl	AccessControl.lean	onlyMinters 修飾子。minters[msg.sender] が偽なら revert する権限ガード。	対象外	4
onlyMinterAdmin	def	AccessControl	AccessControl.lean	onlyMinterAdmin 修飾子。msg.sender ≠ minterAdmin なら revert する権限ガード。	対象外	5
onlyAllowlister	def	AccessControl	AccessControl.lean	onlyAllowlister 修飾子。msg.sender ≠ allowlister なら revert する権限ガード。	対象外	5
transferOwnership	def	AccessControl	AccessControl.lean	transferOwnership(newOwner)：owner のみが所有権を移転できる関数。	対象外	7
pause	def	AccessControl	AccessControl.lean	pause()：コントラクト全体を一時停止する関数（pauser 限定）。	対象外	5
unpause	def	AccessControl	AccessControl.lean	unpause()：一時停止を解除する関数（pauser 限定）。	対象外	5
updatePauser	def	AccessControl	AccessControl.lean	updatePauser(newPauser)：pauser ロールを付け替える関数（owner 限定）。	対象外	8
blocklist	def	AccessControl	AccessControl.lean	blocklist(account)：account をブロックリスト登録する関数（blocklister 限定）。	対象外	7
unBlocklist	def	AccessControl	AccessControl.lean	unBlocklist(account)：account のブロックリスト登録を解除する関数（blocklister 限定）。	対象外	7
updateBlocklister	def	AccessControl	AccessControl.lean	updateBlocklister(newBlocklister)：blocklister ロールを付け替える関数（owner 限定）。	対象外	8
configureMinter	def	AccessControl	AccessControl.lean	configureMinter(minter,amount)：minter を許容額付きで有効化する関数（minterAdmin 限定）。	対象外	9
removeMinter	def	AccessControl	AccessControl.lean	removeMinter(minter)：minter を無効化し許容額を 0 にする関数（minterAdmin 限定）。	対象外	8
mint	def	AccessControl	AccessControl.lean	mint(_to,_amount)：許容額の範囲で新規発行する関数（minter 限定、checkAllowlist 付き）。	対象外	16
burn	def	AccessControl	AccessControl.lean	burn(_amount)：呼び出し元が自身のトークンを焼却する関数（minter 限定）。	対象外	11
updateMinterAdmin	def	AccessControl	AccessControl.lean	updateMinterAdmin(newMinterAdmin)：minterAdmin ロールを付け替える関数（owner 限定）。	対象外	8
allowlist	def	AccessControl	AccessControl.lean	allowlist(account)：account を許可登録する関数（allowlister 限定）。	対象外	8
unAllowlist	def	AccessControl	AccessControl.lean	unAllowlist(account)：account の許可登録を解除する関数（allowlister 限定）。	対象外	7
updateAllowlister	def	AccessControl	AccessControl.lean	updateAllowlister(newAllowlister)：allowlister ロールを付け替える関数（owner 限定）。	対象外	8
owner	def	AccessControl	AccessControl.lean	owner()：現在の所有者アドレスを返す読み取り専用ビュー。	対象外	2
isBlocklisted	def	AccessControl	AccessControl.lean	isBlocklisted(account)：ブロックリスト登録状態を返す読み取り専用ビュー。	対象外	3
isAllowlisted	def	AccessControl	AccessControl.lean	isAllowlisted(account)：許可登録状態を返す読み取り専用ビュー。	対象外	3
isMinter	def	AccessControl	AccessControl.lean	isMinter(account)：minter かどうかを返す読み取り専用ビュー。	対象外	2
minterAllowance	def	AccessControl	AccessControl.lean	minterAllowance(minter)：minter の残り発行許容額を返す読み取り専用ビュー。	対象外	3
setTotalSupply_totalSupply	theorem	AccessControl	AccessControlTheorems.lean	setTotalSupply 後の totalSupply は設定値になる、という補題。	対象外	3
setTotalSupply_balances	theorem	AccessControl	AccessControlTheorems.lean	setTotalSupply は balances を変えない、という frame 補題。	対象外	4
setMinterAllowed_balances	theorem	AccessControl	AccessControlTheorems.lean	setMinterAllowed は balances を変えない、という frame 補題。	対象外	4
setMinterAllowed_totalSupply	theorem	AccessControl	AccessControlTheorems.lean	setMinterAllowed は totalSupply を変えない、という frame 補題。	対象外	4
setMinterAllowed_self	theorem	AccessControl	AccessControlTheorems.lean	setMinterAllowed 後、当該 minter の minterAllowed が設定値になる、という補題。	対象外	4
setMinter_minters_self	theorem	AccessControl	AccessControlTheorems.lean	setMinter 後、当該アドレスの minters フラグが設定値になる、という補題。	対象外	3
setBlocklisted_self	theorem	AccessControl	AccessControlTheorems.lean	setBlocklisted 後、当該アドレスの blocklisted フラグが設定値になる、という補題。	対象外	4
setAllowlisted_self	theorem	AccessControl	AccessControlTheorems.lean	setAllowlisted 後、当該アドレスの allowlisted フラグが設定値になる、という補題。	対象外	4
req_ok	theorem	AccessControl	AccessControlTheorems.lean	req c e が .ok () になるなら条件 c が成立している、という補題。	対象外	2
checkAllowlist_bind_cap	theorem	AccessControl	AccessControlTheorems.lean	上限超の額で checkAllowlist が通れば当該口座は許可登録済み、という補題（V2 cap 分岐）。	対象外	8
WF_setBlocklisted	theorem	AccessControl	AccessControlTheorems.lean	0/1 を書く限り setBlocklisted は WF を保つ、という補題。	対象外	5
WF_setAllowlisted	theorem	AccessControl	AccessControlTheorems.lean	0/1 を書く限り setAllowlisted は WF を保つ、という補題。	対象外	5
toNat_single_update	theorem	AccessControl	AccessControlTheorems.lean	一点更新を toNat で押し通すための補題（toNat_double_update の単点版）。	対象外	2
sum_update_split	theorem	AccessControl	AccessControlTheorems.lean	一点更新前後の総和を omega 向けに等式化した補題。	対象	2
totalBalances_setBalance	theorem	AccessControl	AccessControlTheorems.lean	1 回の setBalance が totalBalances に与える効果を自然数上で釣り合わせた補題。	対象	8
transferOwnership_ok	theorem	AccessControl	AccessControlTheorems.lean	成功した transferOwnership を順方向に特徴づける補助補題。	対象外	9
transferOwnership_auth	theorem	AccessControl	AccessControlTheorems.lean	成功した transferOwnership は owner が呼んだことを含意する（権限）。	対象	8
transferOwnership_unauthorized	theorem	AccessControl	AccessControlTheorems.lean	owner でない呼び出し元は notOwner で revert する（権限・revert形）。	対象	8
transferOwnership_sets_owner	theorem	AccessControl	AccessControlTheorems.lean	成功した transferOwnership は所有者を newOwner に設定する（かつ非ゼロ＝所有権放棄不可）。	対象	8
transferOwnership_wf	theorem	AccessControl	AccessControlTheorems.lean	transferOwnership は健全性不変条件 WF を保つ、という定理。	対象	13
transferOwnership_conserves	theorem	AccessControl	AccessControlTheorems.lean	transferOwnership は供給保存不変条件 SupplyConserved を保つ、という定理。	対象	10
pause_ok	theorem	AccessControl	AccessControlTheorems.lean	成功した pause を順方向に特徴づける補助補題。	対象外	7
unpause_ok	theorem	AccessControl	AccessControlTheorems.lean	成功した unpause を順方向に特徴づける補助補題。	対象外	7
pause_auth	theorem	AccessControl	AccessControlTheorems.lean	pause・unpause の成功は pauser が呼んだことを含意する（権限）。	対象	7
unpause_auth	theorem	AccessControl	AccessControlTheorems.lean	成功した unpause は pauser が呼んだことを含意する（権限）。	対象	7
pause_unauthorized	theorem	AccessControl	AccessControlTheorems.lean	pauser でない呼び出し元は notPauser で revert する（権限・revert形）。	対象	8
unpause_unauthorized	theorem	AccessControl	AccessControlTheorems.lean	pauser でない呼び出し元の unpause は notPauser で revert する。	対象	8
pause_sets_paused	theorem	AccessControl	AccessControlTheorems.lean	pause は paused を true に、unpause は false にする（効果）。	対象	7
unpause_sets_unpaused	theorem	AccessControl	AccessControlTheorems.lean	成功した unpause は paused を false にする（効果）。	対象	7
pause_wf	theorem	AccessControl	AccessControlTheorems.lean	pause は健全性不変条件 WF を保つ、という定理。	対象	12
unpause_wf	theorem	AccessControl	AccessControlTheorems.lean	unpause は健全性不変条件 WF を保つ、という定理。	対象	12
pause_conserves	theorem	AccessControl	AccessControlTheorems.lean	pause は供給保存不変条件 SupplyConserved を保つ、という定理。	対象	9
unpause_conserves	theorem	AccessControl	AccessControlTheorems.lean	unpause は供給保存不変条件 SupplyConserved を保つ、という定理。	対象	9
updatePauser_ok	theorem	AccessControl	AccessControlTheorems.lean	成功した updatePauser を順方向に特徴づける補助補題。	対象外	9
updatePauser_auth	theorem	AccessControl	AccessControlTheorems.lean	ロール付け替え updatePauser の成功は owner が呼んだことを含意する（権限）。	対象	8
updatePauser_wf	theorem	AccessControl	AccessControlTheorems.lean	updatePauser は健全性不変条件 WF を保つ、という定理。	対象	13
blocklist_ok	theorem	AccessControl	AccessControlTheorems.lean	成功した blocklist を順方向に特徴づける補助補題。	対象外	8
unBlocklist_ok	theorem	AccessControl	AccessControlTheorems.lean	成功した unBlocklist を順方向に特徴づける補助補題。	対象外	8
blocklist_auth	theorem	AccessControl	AccessControlTheorems.lean	(un)blocklist の成功は blocklister が呼んだことを含意する（権限）。	対象	8
unBlocklist_auth	theorem	AccessControl	AccessControlTheorems.lean	成功した unBlocklist は blocklister が呼んだことを含意する（権限）。	対象	8
blocklist_unauthorized	theorem	AccessControl	AccessControlTheorems.lean	blocklister でない呼び出し元は notBlocklister で revert する（権限・revert形）。	対象	9
unBlocklist_unauthorized	theorem	AccessControl	AccessControlTheorems.lean	blocklister でない呼び出し元の unBlocklist は notBlocklister で revert する。	対象	9
blocklist_sets	theorem	AccessControl	AccessControlTheorems.lean	blocklist はフラグを 1 に、unBlocklist は 0 にする（効果）。	対象	9
unBlocklist_clears	theorem	AccessControl	AccessControlTheorems.lean	成功した unBlocklist はブロックリストフラグを 0 に戻す（効果）。	対象	9
blocklist_wf	theorem	AccessControl	AccessControlTheorems.lean	blocklist は健全性不変条件 WF を保つ、という定理。	対象	10
unBlocklist_wf	theorem	AccessControl	AccessControlTheorems.lean	unBlocklist は健全性不変条件 WF を保つ、という定理。	対象	10
blocklist_conserves	theorem	AccessControl	AccessControlTheorems.lean	blocklist は供給保存不変条件 SupplyConserved を保つ、という定理。	対象	9
unBlocklist_conserves	theorem	AccessControl	AccessControlTheorems.lean	unBlocklist は供給保存不変条件 SupplyConserved を保つ、という定理。	対象	9
updateBlocklister_ok	theorem	AccessControl	AccessControlTheorems.lean	成功した updateBlocklister を順方向に特徴づける補助補題。	対象外	9
updateBlocklister_auth	theorem	AccessControl	AccessControlTheorems.lean	ロール付け替え updateBlocklister の成功は owner が呼んだことを含意する（権限）。	対象	8
updateBlocklister_wf	theorem	AccessControl	AccessControlTheorems.lean	updateBlocklister は健全性不変条件 WF を保つ、という定理。	対象	13
configureMinter_ok	theorem	AccessControl	AccessControlTheorems.lean	成功した configureMinter を順方向に特徴づける補助補題。	対象外	10
removeMinter_ok	theorem	AccessControl	AccessControlTheorems.lean	成功した removeMinter を順方向に特徴づける補助補題。	対象外	9
configureMinter_auth	theorem	AccessControl	AccessControlTheorems.lean	minter の構成・削除の成功は minterAdmin が呼んだことを含意する（権限）。	対象	9
removeMinter_auth	theorem	AccessControl	AccessControlTheorems.lean	成功した removeMinter は minterAdmin が呼んだことを含意する（権限）。	対象	9
removeMinter_unauthorized	theorem	AccessControl	AccessControlTheorems.lean	minterAdmin でない呼び出し元の removeMinter は notMinterAdmin で revert する。	対象	10
configureMinter_sets	theorem	AccessControl	AccessControlTheorems.lean	configureMinter は minter を許容額付きで有効化、removeMinter は無効化し許容額を 0 にする（効果）。	対象	11
removeMinter_clears	theorem	AccessControl	AccessControlTheorems.lean	成功した removeMinter は minter を無効化し許容額を 0 にする（効果）。	対象	11
configureMinter_wf	theorem	AccessControl	AccessControlTheorems.lean	configureMinter は健全性不変条件 WF を保つ、という定理。	対象	13
removeMinter_wf	theorem	AccessControl	AccessControlTheorems.lean	removeMinter は健全性不変条件 WF を保つ、という定理。	対象	13
configureMinter_conserves	theorem	AccessControl	AccessControlTheorems.lean	configureMinter は供給保存不変条件 SupplyConserved を保つ、という定理。	対象	10
removeMinter_conserves	theorem	AccessControl	AccessControlTheorems.lean	removeMinter は供給保存不変条件 SupplyConserved を保つ、という定理。	対象	10
updateMinterAdmin_ok	theorem	AccessControl	AccessControlTheorems.lean	成功した updateMinterAdmin を順方向に特徴づける補助補題。	対象外	9
updateMinterAdmin_auth	theorem	AccessControl	AccessControlTheorems.lean	ロール付け替え updateMinterAdmin の成功は owner が呼んだことを含意する（権限）。	対象	8
updateMinterAdmin_wf	theorem	AccessControl	AccessControlTheorems.lean	updateMinterAdmin は健全性不変条件 WF を保つ、という定理。	対象	13
mint_eq	theorem	AccessControl	AccessControlTheorems.lean	成功した mint の算術的書き込みと結果状態を順方向に特徴づける補題。	対象外	17
mint_guards	theorem	AccessControl	AccessControlTheorems.lean	成功した mint のガード事実（minter であること・非ブロックリスト・上限超は許可登録）をまとめた補題。	対象外	17
mint_auth	theorem	AccessControl	AccessControlTheorems.lean	mint の成功は構成済み minter が呼んだことを含意する（権限）。	対象	8
mint_totalSupply	theorem	AccessControl	AccessControlTheorems.lean	mint は totalSupply を amount だけ増やす（桁あふれなし）、という定理（効果・供給）。	対象	13
mint_balance	theorem	AccessControl	AccessControlTheorems.lean	mint は受取人の残高を amount だけ増やす、という定理（効果・残高）。	対象	13
mint_minterAllowed	theorem	AccessControl	AccessControlTheorems.lean	mint は minterAllowed を超えられず、成功時は残り許容額が amount 減る、という定理（上限）。	対象	15
mint_frame	theorem	AccessControl	AccessControlTheorems.lean	mint は受取人以外の残高を変えない、という frame 定理。	対象	12
mint_totalBalances	theorem	AccessControl	AccessControlTheorems.lean	成功した mint は totalBalances を amount だけ増やす、という補題。	対象外	15
mint_conserves	theorem	AccessControl	AccessControlTheorems.lean	mint は供給保存不変条件 SupplyConserved を保つ、という定理。	対象	10
mint_wf	theorem	AccessControl	AccessControlTheorems.lean	mint は健全性不変条件 WF を保つ、という定理。	対象	16
burn_eq	theorem	AccessControl	AccessControlTheorems.lean	成功した burn の算術的書き込みと結果状態を順方向に特徴づける補題。	対象外	11
burn_guards	theorem	AccessControl	AccessControlTheorems.lean	成功した burn のガード事実をまとめた補題。	対象外	10
burn_auth	theorem	AccessControl	AccessControlTheorems.lean	burn の成功は構成済み minter が呼んだことを含意する（権限）。	対象	6
burn_totalSupply	theorem	AccessControl	AccessControlTheorems.lean	burn は totalSupply を amount だけ減らす（桁借りなし）、という定理（効果・供給）。	対象	11
burn_balance	theorem	AccessControl	AccessControlTheorems.lean	burn は呼び出し元の残高を amount だけ減らす、という定理（効果・残高）。	対象	12
burn_frame	theorem	AccessControl	AccessControlTheorems.lean	burn は呼び出し元以外の残高を変えない、という frame 定理。	対象	10
burn_totalBalances	theorem	AccessControl	AccessControlTheorems.lean	成功した burn は totalBalances を amount だけ減らす、という補題。	対象外	13
burn_conserves	theorem	AccessControl	AccessControlTheorems.lean	burn は供給保存不変条件 SupplyConserved を保つ、という定理。	対象	9
burn_wf	theorem	AccessControl	AccessControlTheorems.lean	burn は健全性不変条件 WF を保つ、という定理。	対象	14
allowlist_ok	theorem	AccessControl	AccessControlTheorems.lean	成功した allowlist を順方向に特徴づける補助補題。	対象外	9
unAllowlist_ok	theorem	AccessControl	AccessControlTheorems.lean	成功した unAllowlist を順方向に特徴づける補助補題。	対象外	8
allowlist_auth	theorem	AccessControl	AccessControlTheorems.lean	(un)allowlist の成功は allowlister が呼んだことを含意する（権限）。	対象	8
unAllowlist_auth	theorem	AccessControl	AccessControlTheorems.lean	成功した unAllowlist は allowlister が呼んだことを含意する（権限）。	対象外	8
unAllowlist_unauthorized	theorem	AccessControl	AccessControlTheorems.lean	allowlister でない呼び出し元の unAllowlist は revert する（権限・revert形）。	対象外	9
allowlist_sets	theorem	AccessControl	AccessControlTheorems.lean	allowlist はフラグを 1 に、unAllowlist は 0 にする（効果）。	対象	9
unAllowlist_clears	theorem	AccessControl	AccessControlTheorems.lean	成功した unAllowlist は許可登録フラグを 0 に戻す（効果）。	対象	9
allowlist_wf	theorem	AccessControl	AccessControlTheorems.lean	allowlist は健全性不変条件 WF を保つ、という定理。	対象	10
unAllowlist_wf	theorem	AccessControl	AccessControlTheorems.lean	unAllowlist は健全性不変条件 WF を保つ、という定理。	対象	10
allowlist_conserves	theorem	AccessControl	AccessControlTheorems.lean	allowlist は供給保存不変条件 SupplyConserved を保つ、という定理。	対象	9
unAllowlist_conserves	theorem	AccessControl	AccessControlTheorems.lean	unAllowlist は供給保存不変条件 SupplyConserved を保つ、という定理。	対象	9
updateAllowlister_ok	theorem	AccessControl	AccessControlTheorems.lean	成功した updateAllowlister を順方向に特徴づける補助補題。	対象外	9
updateAllowlister_auth	theorem	AccessControl	AccessControlTheorems.lean	ロール付け替え updateAllowlister の成功は owner が呼んだことを含意する（権限）。	対象	8
updateAllowlister_wf	theorem	AccessControl	AccessControlTheorems.lean	updateAllowlister は健全性不変条件 WF を保つ、という定理。	対象	13
whenNotPaused_paused	theorem	AccessControl	AccessControlTheorems.lean	paused 状態では whenNotPaused は revert する、という補題。	対象	4
transfer_paused	theorem	AccessControl	AccessControlTheorems.lean	paused 状態では transfer は Pausable: paused で revert する、という定理。	対象	10
transferFrom_paused	theorem	AccessControl	AccessControlTheorems.lean	paused 状態では transferFrom は Pausable: paused で revert する、という定理。	対象	11
approve_paused	theorem	AccessControl	AccessControlTheorems.lean	paused 状態では approve は Pausable: paused で revert する、という定理。	対象	10
increaseAllowance_paused	theorem	AccessControl	AccessControlTheorems.lean	paused 状態では increaseAllowance は Pausable: paused で revert する、という定理。	対象	11
decreaseAllowance_paused	theorem	AccessControl	AccessControlTheorems.lean	paused 状態では decreaseAllowance は Pausable: paused で revert する、という定理。	対象	9
mint_paused	theorem	AccessControl	AccessControlTheorems.lean	paused 状態では mint は Pausable: paused で revert する、という定理。	対象	18
burn_paused	theorem	AccessControl	AccessControlTheorems.lean	paused 状態では burn は Pausable: paused で revert する、という定理。	対象	13
configureMinter_paused	theorem	AccessControl	AccessControlTheorems.lean	paused 状態では configureMinter は Pausable: paused で revert する、という定理。	対象	11
allowlist_paused	theorem	AccessControl	AccessControlTheorems.lean	paused 状態では allowlist は Pausable: paused で revert する、という定理。	対象	10
transfer_guards	theorem	AccessControl	AccessControlTheorems.lean	成功した transfer のガード事実をまとめた補題。	対象外	11
transferFrom_guards	theorem	AccessControl	AccessControlTheorems.lean	成功した transferFrom のガード事実をまとめた補題。	対象外	12
transfer_not_blocklisted	theorem	AccessControl	AccessControlTheorems.lean	transfer の成功は送り手・受け手の誰もブロックリストされていないことを含意する。	対象	8
transferFrom_not_blocklisted	theorem	AccessControl	AccessControlTheorems.lean	transferFrom の成功は spender・payer・payee がいずれも非ブロックリストであることを含意する。	対象	8
mint_not_blocklisted	theorem	AccessControl	AccessControlTheorems.lean	mint の成功は呼び出し元と受取人が非ブロックリストであることを含意する。	対象	8
burn_not_blocklisted	theorem	AccessControl	AccessControlTheorems.lean	burn の成功は呼び出し元が非ブロックリストであることを含意する。	対象	6
transfer_above_cap_allowlisted	theorem	AccessControl	AccessControlTheorems.lean	上限超の transfer 成功は送り手が許可登録済みであることを含意する。	対象	8
transferFrom_above_cap_allowlisted	theorem	AccessControl	AccessControlTheorems.lean	上限超の transferFrom 成功は payer(from) が許可登録済みであることを含意する。	対象	8
mint_above_cap_allowlisted	theorem	AccessControl	AccessControlTheorems.lean	上限超の mint 成功は呼び出し元が許可登録済みであることを含意する。	対象	8
transferOwnership_revert_noop	theorem	AccessControl	AccessControlTheorems.lean	transferOwnership が revert した場合、状態は一切変化しない、という定理。	対象	6
pause_revert_noop	theorem	AccessControl	AccessControlTheorems.lean	pause が revert した場合、状態は一切変化しない、という定理。	対象	5
unpause_revert_noop	theorem	AccessControl	AccessControlTheorems.lean	unpause が revert した場合、状態は一切変化しない、という定理。	対象	5
updatePauser_revert_noop	theorem	AccessControl	AccessControlTheorems.lean	updatePauser が revert した場合、状態は一切変化しない、という定理。	対象	6
blocklist_revert_noop	theorem	AccessControl	AccessControlTheorems.lean	blocklist が revert した場合、状態は一切変化しない、という定理。	対象	6
unBlocklist_revert_noop	theorem	AccessControl	AccessControlTheorems.lean	unBlocklist が revert した場合、状態は一切変化しない、という定理。	対象	6
updateBlocklister_revert_noop	theorem	AccessControl	AccessControlTheorems.lean	updateBlocklister が revert した場合、状態は一切変化しない、という定理。	対象	6
configureMinter_revert_noop	theorem	AccessControl	AccessControlTheorems.lean	configureMinter が revert した場合、状態は一切変化しない、という定理。	対象	7
removeMinter_revert_noop	theorem	AccessControl	AccessControlTheorems.lean	removeMinter が revert した場合、状態は一切変化しない、という定理。	対象	6
mint_revert_noop	theorem	AccessControl	AccessControlTheorems.lean	mint が revert した場合、状態は一切変化しない、という定理。	対象	7
burn_revert_noop	theorem	AccessControl	AccessControlTheorems.lean	burn が revert した場合、状態は一切変化しない、という定理。	対象	6
updateMinterAdmin_revert_noop	theorem	AccessControl	AccessControlTheorems.lean	updateMinterAdmin が revert した場合、状態は一切変化しない、という定理。	対象	6
allowlist_revert_noop	theorem	AccessControl	AccessControlTheorems.lean	allowlist が revert した場合、状態は一切変化しない、という定理。	対象	6
unAllowlist_revert_noop	theorem	AccessControl	AccessControlTheorems.lean	unAllowlist が revert した場合、状態は一切変化しない、という定理。	対象	6
updateAllowlister_revert_noop	theorem	AccessControl	AccessControlTheorems.lean	updateAllowlister が revert した場合、状態は一切変化しない、という定理。	対象	6
updatePauser_unauthorized	theorem	AccessControl	AccessControlTheorems.lean	owner でない呼び出し元は updatePauser を notOwner で revert する（権限・revert形）。	対象	9
updateBlocklister_unauthorized	theorem	AccessControl	AccessControlTheorems.lean	owner でない呼び出し元は updateBlocklister を notOwner で revert する（権限・revert形）。	対象	9
updateMinterAdmin_unauthorized	theorem	AccessControl	AccessControlTheorems.lean	owner でない呼び出し元は updateMinterAdmin を notOwner で revert する（権限・revert形）。	対象	9
updateAllowlister_unauthorized	theorem	AccessControl	AccessControlTheorems.lean	owner でない呼び出し元は updateAllowlister を notOwner で revert する（権限・revert形）。	対象	9
Address	abbrev	Foundation	Address.lean	Solidity の address を表す語型（BitVec 160）。	対象外	0
Address.zero	def	Foundation	Address.lean	ゼロアドレス address(0)。多くのガードが拒否する特別な値。	対象外	1
CallContext	structure	Foundation	Address.lean	モデルが依存する msg.sender・block.timestamp・block.chainid をまとめた呼び出し文脈。	対象外	0
State.setBalance	def	ERC20	ERC20.lean	balances[a] を v に書き換える純粋な状態更新関数。	対象外	3
State.setAllowance	def	ERC20	ERC20.lean	allowed[owner][spender] を v に書き換える純粋な状態更新関数。	対象外	3
req	def	ERC20	ERC20.lean	require(cond, err) のモデル。cond が真なら続行、偽なら err で revert する。	対象外	1
whenNotPaused	def	ERC20	ERC20.lean	whenNotPaused 修飾子。paused なら Pausable: paused で revert するガード。	対象外	3
notBlocklisted	def	ERC20	ERC20.lean	notBlocklisted(account) 修飾子。account がブロックリスト登録なら revert するガード。	対象外	5
checkAllowlist	def	ERC20	ERC20.lean	checkAllowlist(account,value) 修飾子（V2）。上限超の額は account の許可登録を要求する。	対象外	6
balanceOf	def	ERC20	ERC20.lean	balanceOf(account)：口座残高を返す読み取り専用ビュー。	対象外	3
totalSupply	def	ERC20	ERC20.lean	totalSupply()：総供給量を返す読み取り専用ビュー。	対象外	2
allowance	def	ERC20	ERC20.lean	allowance(owner,spender)：承認額を返す読み取り専用ビュー。	対象外	3
approve	def	ERC20	ERC20.lean	approve(spender,value)：承認額を value に設定する関数。	対象外	8
increaseAllowance	def	ERC20	ERC20.lean	increaseAllowance(spender,increment)：承認額をチェック付きで増やす関数。	対象外	9
decreaseAllowance	def	ERC20	ERC20.lean	decreaseAllowance(spender,decrement)：承認額をチェック付きで減らす関数（checkAllowlist なし）。	対象外	7
transfer	def	ERC20	ERC20.lean	transfer(to,value)：各ガードを通過後に _transfer で送金する関数。	対象外	8
allowanceStep	def	ERC20	ERC20.lean	transferFrom の承認消費ステップ。無限承認は据え置き、有限なら value を引く。	対象外	8
transferFrom	def	ERC20	ERC20.lean	transferFrom(from,to,value)：承認を allowanceStep で処理後、_transfer で送金する関数。	対象外	9
req_bind	theorem	ERC20	ERC20Theorems.lean	require の後続処理：条件成立なら f() に進み、不成立なら revert に短絡する、という補題。	対象外	2
ok_bind	theorem	ERC20	ERC20Theorems.lean	Except.ok の bind は値を後続へ渡すだけ、という（do ブロック書き換え用の）補題。	対象外	1
error_bind	theorem	ERC20	ERC20Theorems.lean	Except.error は bind を短絡する、という補題。	対象外	1
pure_eq	theorem	ERC20	ERC20Theorems.lean	Except Error における pure は Except.ok である、という補題。	対象外	1
bind_eq_ok	theorem	ERC20	ERC20Theorems.lean	bind の成功は前段の成功と後続の成功に分解できる、という補題。	対象外	3
req_bind_eq_ok	theorem	ERC20	ERC20Theorems.lean	do ブロック先頭の require を 1 つ剥がす補題：成功は条件を強制し後続を成功させる。	対象外	3
checkAllowlist_bind_eq_ok	theorem	ERC20	ERC20Theorems.lean	checkAllowlist は状態を変えないので、成功時は後続が同じ状態で成功する、という補題。	対象外	10
setBalance_balances	theorem	ERC20	ERC20Theorems.lean	setBalance 後の balances は当該アドレスだけが書き換わる点更新になる、という補題。	対象外	4
setBalance_totalSupply	theorem	ERC20	ERC20Theorems.lean	setBalance は totalSupply を変えない、という frame 補題。	対象外	4
setBalance_allowed	theorem	ERC20	ERC20Theorems.lean	setBalance は allowed を変えない、という frame 補題。	対象外	4
setBalance_blocklisted	theorem	ERC20	ERC20Theorems.lean	setBalance は blocklisted を変えない、という frame 補題。	対象外	4
setBalance_allowlisted	theorem	ERC20	ERC20Theorems.lean	setBalance は allowlisted を変えない、という frame 補題。	対象外	4
setBalance_authorizationStates	theorem	ERC20	ERC20Theorems.lean	setBalance は authorizationStates を変えない、という frame 補題。	対象外	5
setBalance_initializedVersion	theorem	ERC20	ERC20Theorems.lean	setBalance は initializedVersion を変えない、という frame 補題。	対象外	5
setAllowance_balances	theorem	ERC20	ERC20Theorems.lean	setAllowance は balances を変えない、という frame 補題。	対象外	4
setAllowance_totalSupply	theorem	ERC20	ERC20Theorems.lean	setAllowance は totalSupply を変えない、という frame 補題。	対象外	4
setAllowance_blocklisted	theorem	ERC20	ERC20Theorems.lean	setAllowance は blocklisted を変えない、という frame 補題。	対象外	4
setAllowance_allowlisted	theorem	ERC20	ERC20Theorems.lean	setAllowance は allowlisted を変えない、という frame 補題。	対象外	4
setAllowance_authorizationStates	theorem	ERC20	ERC20Theorems.lean	setAllowance は authorizationStates を変えない、という frame 補題。	対象外	5
setAllowance_initializedVersion	theorem	ERC20	ERC20Theorems.lean	setAllowance は initializedVersion を変えない、という frame 補題。	対象外	5
setAllowance_allowed_self	theorem	ERC20	ERC20Theorems.lean	setAllowance 後、当該 (owner,spender) の allowed が設定値になる、という補題。	対象外	4
State.afterCall	def	ERC20	ERC20Theorems.lean	呼び出し結果を EVM ロールバック付きで観測する関数：revert 時は前状態を保つ。	対象	2
afterCall_error	theorem	ERC20	ERC20Theorems.lean	revert した呼び出しは観測される状態を変えない、という補題。	対象	3
transferResult	def	ERC20	ERC20Theorems.lean	成功した _transfer の結果状態：frm を value だけ引き、引いた後の状態から dst に足す。	対象外	4
toNat_double_update	theorem	ERC20	ERC20Theorems.lean	二点同時更新を toNat で押し通すための補題。	対象外	2
sum_double_update_nat	theorem	ERC20	ERC20Theorems.lean	二点を書き換えても対の合計が不変なら、有限和の総計も不変である、という補題。	対象外	2
WF.of_flags_eq	theorem	ERC20	ERC20Theorems.lean	WF はフラグ写像と initializedVersion だけに依存し、それらを保つ遷移は WF を保つ、という補題。	対象外	6
transfer_eq_ok	theorem	ERC20	ERC20Theorems.lean	成功した transfer は呼び出し元からの _transfer の成功に還元される、という補題。	対象外	10
wf_transfer	theorem	ERC20	ERC20Theorems.lean	transfer は健全性不変条件 WF を保つ、という定理。	対象	8
transfer_conserves	theorem	ERC20	ERC20Theorems.lean	transfer は供給保存不変条件 SupplyConserved を保つ、という定理。	対象	8
transfer_totalSupply	theorem	ERC20	ERC20Theorems.lean	成功した transfer は totalSupply を変えない、という定理。	対象	7
transfer_frame	theorem	ERC20	ERC20Theorems.lean	transfer は from・to 以外の口座残高を変えない、という frame 定理。	対象	7
transfer_self	theorem	ERC20	ERC20Theorems.lean	from == to の transfer は全残高を変えない（自己送金の安全性）、という定理。	対象	7
transfer_le	theorem	ERC20	ERC20Theorems.lean	成功した transfer は呼び出し元の残高を桁借りしない（value ≤ 残高）、という定理。	対象	7
transferFrom_eq_ok	theorem	ERC20	ERC20Theorems.lean	成功した transferFrom が承認ステップ s₁ と _transfer に分解される、という補題。	対象外	16
transferFrom_step_balances	theorem	ERC20	ERC20Theorems.lean	承認ステップは残高も totalSupply も触らないので s₁ は s と同じ供給事実を満たす、という補題。	対象外	10
transferFrom_conserves	theorem	ERC20	ERC20Theorems.lean	承認ステップが残高を保つので、transferFrom の保存は _transfer の保存に還元される、という定理。	対象	14
transferFrom_totalSupply	theorem	ERC20	ERC20Theorems.lean	成功した transferFrom は totalSupply を変えない、という定理。	対象	11
wf_transferFrom	theorem	ERC20	ERC20Theorems.lean	transferFrom は健全性不変条件 WF を保つ、という定理。	対象	11
transferFrom_allowance	theorem	ERC20	ERC20Theorems.lean	承認が有限なら transferFrom は allowed を value だけ減らし、無限承認は据え置く（承認整合性）。	対象	10
approve_eq_ok	theorem	ERC20	ERC20Theorems.lean	成功した approve は呼び出し元からの _approve に還元される、という補題。	対象外	10
wf_approve	theorem	ERC20	ERC20Theorems.lean	approve は健全性不変条件 WF を保つ、という定理。	対象	8
approve_conserves	theorem	ERC20	ERC20Theorems.lean	approve は供給保存不変条件 SupplyConserved を保つ、という定理。	対象	8
approve_allowance	theorem	ERC20	ERC20Theorems.lean	成功した approve は allowed[msg.sender][spender] を value に設定する、という定理。	対象	10
wf_increaseAllowance	theorem	ERC20	ERC20Theorems.lean	increaseAllowance は健全性不変条件 WF を保つ、という定理。	対象	13
wf_decreaseAllowance	theorem	ERC20	ERC20Theorems.lean	decreaseAllowance は健全性不変条件 WF を保つ、という定理。	対象	11
transfer_revert_noop	theorem	ERC20	ERC20Theorems.lean	transfer が revert した場合、状態は一切変化しない、という定理。	対象	7
transferFrom_revert_noop	theorem	ERC20	ERC20Theorems.lean	transferFrom が revert した場合、状態は一切変化しない、という定理。	対象	7
approve_revert_noop	theorem	ERC20	ERC20Theorems.lean	approve が revert した場合、状態は一切変化しない、という定理。	対象	7
increaseAllowance_revert_noop	theorem	ERC20	ERC20Theorems.lean	increaseAllowance が revert した場合、状態は一切変化しない、という定理。	対象	7
decreaseAllowance_revert_noop	theorem	ERC20	ERC20Theorems.lean	decreaseAllowance が revert した場合、状態は一切変化しない、という定理。	対象	7
increaseAllowance_eq_ok	theorem	ERC20	ERC20Theorems.lean	成功した increaseAllowance は呼び出し元からの _increaseAllowance に還元される、という補題。	対象外	12
increaseAllowance_allowance	theorem	ERC20	ERC20Theorems.lean	成功した increaseAllowance は allowed[msg.sender][spender] を increment 分（checked）増やす、という効果定理。	対象	13
increaseAllowance_conserves	theorem	ERC20	ERC20Theorems.lean	increaseAllowance は供給保存不変条件 SupplyConserved を保つ、という定理。	対象	10
decreaseAllowance_eq_ok	theorem	ERC20	ERC20Theorems.lean	成功した decreaseAllowance は呼び出し元からの _decreaseAllowance に還元される、という補題。	対象外	8
decreaseAllowance_allowance	theorem	ERC20	ERC20Theorems.lean	成功した decreaseAllowance は allowed[msg.sender][spender] を decrement 分（checked）減らす、という効果定理。	対象	15
decreaseAllowance_conserves	theorem	ERC20	ERC20Theorems.lean	decreaseAllowance は供給保存不変条件 SupplyConserved を保つ、という定理。	対象	11
transferFrom_le	theorem	ERC20	ERC20Theorems.lean	成功した transferFrom は支払者の残高を桁借りしない（value ≤ 残高）、という定理。	対象	11
transferFrom_frame	theorem	ERC20	ERC20Theorems.lean	transferFrom は from・to 以外の口座残高を変えない、という frame 定理。	対象	11
transferFrom_self	theorem	ERC20	ERC20Theorems.lean	from == to の transferFrom は全残高を変えない（自己送金の安全性）、という定理。	対象	11
Error	inductive	Foundation	Error.lean	FiatTokenV2 と基底コントラクトの全 revert 理由を列挙した型。同一の理由文字列は単一コンストラクタを共有する。	対象外	0
Error.revertMessage	def	Foundation	Error.lean	各 Error をオンチェーンの revert 理由文字列に 1:1 で対応づける関数。	対象	1
SignedMessage	inductive	Signatures	Signatures.lean	FiatTokenV2 が使う *_TYPEHASH ごとに 1 コンストラクタを持つ EIP-712 型付きメッセージ。	対象外	0
SigOracle	structure	Signatures	Signatures.lean	keccak256/ECDSA 復元を信頼するオラクルとして抽象化した署名プリミティブ一式。	対象外	0
State.setPermitNonce	def	Signatures	Signatures.lean	_permitNonces[owner] を v に書き換える純粋な状態更新関数。	対象外	3
State.setAuthorizationState	def	Signatures	Signatures.lean	_authorizationStates[authorizer][nonce] を v に書き換える純粋な状態更新関数。	対象外	4
nonces	def	Signatures	Signatures.lean	nonces(owner)：EIP-2612 の現在 nonce を返す読み取り専用ビュー。	対象外	3
authorizationState	def	Signatures	Signatures.lean	authorizationState(authorizer,nonce)：認可の使用済み状態を返す読み取り専用ビュー。	対象外	4
domainSeparatorV4	def	Signatures	Signatures.lean	_domainSeparatorV4()：chainid 一致ならキャッシュ値、不一致ならオラクルで再計算するドメイン区切り子。	対象外	5
permit	def	Signatures	Signatures.lean	permit(owner,spender,value,deadline,v,r,s)：署名で承認を設定する EIP-2612 関数。	対象外	11
requireUnusedAuthorization	def	Signatures	Signatures.lean	_requireUnusedAuthorization：認可が未使用であることを要求するガード。	対象外	6
requireValidAuthorization	def	Signatures	Signatures.lean	_requireValidAuthorization：認可が有効期間内かつ未使用であることを要求するガード。	対象外	8
transferWithAuthorization	def	Signatures	Signatures.lean	transferWithAuthorization(...)：署名認可で第三者が送金を実行する EIP-3009 関数。	対象外	11
receiveWithAuthorization	def	Signatures	Signatures.lean	receiveWithAuthorization(...)：受取人自身が呼ぶ必要のある EIP-3009 送金関数。	対象外	11
cancelAuthorization	def	Signatures	Signatures.lean	cancelAuthorization(authorizer,nonce,v,r,s)：署名で未使用認可を取り消す EIP-3009 関数。	対象外	8
req_neg	theorem	Signatures	SignaturesTheorems.lean	条件が偽の require はちょうど revert と一致する、という補題。	対象外	2
req_pos	theorem	Signatures	SignaturesTheorems.lean	条件が真の require は () で続行する、という補題。	対象外	2
setPermitNonce_balances	theorem	Signatures	SignaturesTheorems.lean	setPermitNonce は balances を変えない、という frame 補題。	対象外	4
setPermitNonce_totalSupply	theorem	Signatures	SignaturesTheorems.lean	setPermitNonce は totalSupply を変えない、という frame 補題。	対象外	4
setPermitNonce_blocklisted	theorem	Signatures	SignaturesTheorems.lean	setPermitNonce は blocklisted を変えない、という frame 補題。	対象外	4
setPermitNonce_allowlisted	theorem	Signatures	SignaturesTheorems.lean	setPermitNonce は allowlisted を変えない、という frame 補題。	対象外	4
setPermitNonce_authorizationStates	theorem	Signatures	SignaturesTheorems.lean	setPermitNonce は authorizationStates を変えない、という frame 補題。	対象外	5
setPermitNonce_initializedVersion	theorem	Signatures	SignaturesTheorems.lean	setPermitNonce は initializedVersion を変えない、という frame 補題。	対象外	5
setPermitNonce_self	theorem	Signatures	SignaturesTheorems.lean	setPermitNonce 後、当該 owner の nonce が設定値になる、という補題。	対象外	4
setPermitNonce_permitNonces_ne	theorem	Signatures	SignaturesTheorems.lean	setPermitNonce は当該 owner 以外の nonce を変えない、という補題。	対象外	4
setAllowance_permitNonces	theorem	Signatures	SignaturesTheorems.lean	setAllowance は permitNonces を変えない、という frame 補題。	対象外	4
setBalance_permitNonces	theorem	Signatures	SignaturesTheorems.lean	setBalance は permitNonces を変えない、という frame 補題。	対象外	4
setAuthorizationState_balances	theorem	Signatures	SignaturesTheorems.lean	setAuthorizationState は balances を変えない、という frame 補題。	対象外	5
setAuthorizationState_totalSupply	theorem	Signatures	SignaturesTheorems.lean	setAuthorizationState は totalSupply を変えない、という frame 補題。	対象外	5
setAuthorizationState_allowed	theorem	Signatures	SignaturesTheorems.lean	setAuthorizationState は allowed を変えない、という frame 補題。	対象外	5
setAuthorizationState_blocklisted	theorem	Signatures	SignaturesTheorems.lean	setAuthorizationState は blocklisted を変えない、という frame 補題。	対象外	5
setAuthorizationState_allowlisted	theorem	Signatures	SignaturesTheorems.lean	setAuthorizationState は allowlisted を変えない、という frame 補題。	対象外	5
setAuthorizationState_initializedVersion	theorem	Signatures	SignaturesTheorems.lean	setAuthorizationState は initializedVersion を変えない、という frame 補題。	対象外	6
setAuthorizationState_self	theorem	Signatures	SignaturesTheorems.lean	setAuthorizationState 後、当該 (authorizer,nonce) の状態が設定値になる、という補題。	対象外	5
WF_setAuthorizationState	theorem	Signatures	SignaturesTheorems.lean	0/1 を書く限り setAuthorizationState は WF を保つ、という補題。	対象外	6
permit_eq_ok	theorem	Signatures	SignaturesTheorems.lean	成功した permit は owner からの _permit の成功に還元される、という補題。	対象外	13
permit_guards	theorem	Signatures	SignaturesTheorems.lean	成功した permit のガード事実をまとめた補題。	対象外	14
permit_not_expired	theorem	Signatures	SignaturesTheorems.lean	成功した permit は deadline 内である、という定理（期限）。	対象	13
permit_nonce_increments	theorem	Signatures	SignaturesTheorems.lean	成功した permit は owner の nonce をちょうど 1 増やす、という定理（再生防止）。	対象	17
permit_nonce_frame	theorem	Signatures	SignaturesTheorems.lean	成功した permit は owner 以外の nonce を変えない、という定理（nonce frame）。	対象	17
permit_sets_allowance	theorem	Signatures	SignaturesTheorems.lean	成功した permit は allowed[owner][spender] を value に設定する、という定理（効果）。	対象	16
permit_signed_by_owner	theorem	Signatures	SignaturesTheorems.lean	成功した permit は owner の EIP-712 署名で認可されている、という定理（権限）。	対象	13
permit_wf	theorem	Signatures	SignaturesTheorems.lean	permit は健全性不変条件 WF を保つ、という定理。	対象	15
permit_conserves	theorem	Signatures	SignaturesTheorems.lean	permit は供給保存不変条件 SupplyConserved を保つ、という定理。	対象	14
transferWithAuthorization_eq_ok	theorem	Signatures	SignaturesTheorems.lean	成功した transferWithAuthorization を内部処理に還元する補題。	対象外	13
transferWithAuthorization_guards	theorem	Signatures	SignaturesTheorems.lean	成功した transferWithAuthorization のガード事実をまとめた補題。	対象外	14
transferWithAuthorization_unused	theorem	Signatures	SignaturesTheorems.lean	成功した transferWithAuthorization は (from,nonce) 認可が未使用だったことを要求する（単回使用）。	対象	12
transferWithAuthorization_marks_used	theorem	Signatures	SignaturesTheorems.lean	成功した transferWithAuthorization は (from,nonce) 認可を使用済みにする（単回使用）。	対象	13
transferWithAuthorization_no_replay	theorem	Signatures	SignaturesTheorems.lean	一度消費された (from,nonce) は二度と transferWithAuthorization に使えない（再生不可）。	対象	11
transferWithAuthorization_signed_by_from	theorem	Signatures	SignaturesTheorems.lean	成功した transferWithAuthorization は from の署名で認可されている、という定理（権限）。	対象	12
transferWithAuthorization_within_window	theorem	Signatures	SignaturesTheorems.lean	成功した transferWithAuthorization は (validAfter,validBefore) 内である、という定理（有効期間）。	対象	12
transferWithAuthorization_wf	theorem	Signatures	SignaturesTheorems.lean	transferWithAuthorization は健全性不変条件 WF を保つ、という定理。	対象	14
transferWithAuthorization_conserves	theorem	Signatures	SignaturesTheorems.lean	transferWithAuthorization は供給保存不変条件 SupplyConserved を保つ、という定理。	対象	13
transferWithAuthorization_totalSupply	theorem	Signatures	SignaturesTheorems.lean	transferWithAuthorization は totalSupply を変えない、という定理。	対象	12
receiveWithAuthorization_eq_ok	theorem	Signatures	SignaturesTheorems.lean	成功した receiveWithAuthorization を内部処理に還元する補題。	対象外	13
receiveWithAuthorization_guards	theorem	Signatures	SignaturesTheorems.lean	成功した receiveWithAuthorization のガード事実をまとめた補題。	対象外	14
receiveWithAuthorization_payee	theorem	Signatures	SignaturesTheorems.lean	receiveWithAuthorization の成功は payee が呼び出し元（to == msg.sender）であることを含意する（フロントラン防止）。	対象	12
receiveWithAuthorization_unused	theorem	Signatures	SignaturesTheorems.lean	成功した receiveWithAuthorization は認可が未使用だったことを要求する（単回使用）。	対象	12
receiveWithAuthorization_marks_used	theorem	Signatures	SignaturesTheorems.lean	成功した receiveWithAuthorization は認可を使用済みにする（単回使用）。	対象	13
receiveWithAuthorization_no_replay	theorem	Signatures	SignaturesTheorems.lean	一度消費された認可は二度と receiveWithAuthorization に使えない（再生不可）。	対象	11
receiveWithAuthorization_signed_by_from	theorem	Signatures	SignaturesTheorems.lean	成功した receiveWithAuthorization は from の署名で認可されている、という定理（権限）。	対象	12
receiveWithAuthorization_wf	theorem	Signatures	SignaturesTheorems.lean	receiveWithAuthorization は健全性不変条件 WF を保つ、という定理。	対象	14
receiveWithAuthorization_conserves	theorem	Signatures	SignaturesTheorems.lean	receiveWithAuthorization は供給保存不変条件 SupplyConserved を保つ、という定理。	対象	13
receiveWithAuthorization_totalSupply	theorem	Signatures	SignaturesTheorems.lean	receiveWithAuthorization は totalSupply を変えない、という定理。	対象	12
cancelAuthorization_eq_ok	theorem	Signatures	SignaturesTheorems.lean	成功した cancelAuthorization を内部処理に還元する補題。	対象外	9
cancelAuthorization_unused	theorem	Signatures	SignaturesTheorems.lean	成功した cancelAuthorization は認可が未使用だったことを要求する（単回使用）。	対象	12
cancelAuthorization_marks_used	theorem	Signatures	SignaturesTheorems.lean	成功した cancelAuthorization は認可を使用済みにする（効果）。	対象	13
cancelAuthorization_signed_by_authorizer	theorem	Signatures	SignaturesTheorems.lean	成功した cancelAuthorization は authorizer の署名で認可されている、という定理（権限）。	対象	12
cancelAuthorization_blocks_transfer	theorem	Signatures	SignaturesTheorems.lean	(authorizer,nonce) を取り消した後は、同じ (from,nonce) の transferWithAuthorization は成功しない。	対象	12
cancelAuthorization_wf	theorem	Signatures	SignaturesTheorems.lean	cancelAuthorization は健全性不変条件 WF を保つ、という定理。	対象	14
cancelAuthorization_conserves	theorem	Signatures	SignaturesTheorems.lean	cancelAuthorization は供給保存不変条件 SupplyConserved を保つ、という定理。	対象	13
permit_paused	theorem	Signatures	SignaturesTheorems.lean	paused 状態では permit は Pausable: paused で revert する、という定理。	対象	13
transferWithAuthorization_paused	theorem	Signatures	SignaturesTheorems.lean	paused 状態では transferWithAuthorization は Pausable: paused で revert する、という定理。	対象	13
receiveWithAuthorization_paused	theorem	Signatures	SignaturesTheorems.lean	paused 状態では receiveWithAuthorization は Pausable: paused で revert する、という定理。	対象	13
cancelAuthorization_paused	theorem	Signatures	SignaturesTheorems.lean	paused 状態では cancelAuthorization は Pausable: paused で revert する、という定理。	対象	10
permit_not_blocklisted	theorem	Signatures	SignaturesTheorems.lean	permit の成功は owner・spender が非ブロックリストであることを含意する。	対象	11
transferWithAuthorization_not_blocklisted	theorem	Signatures	SignaturesTheorems.lean	transferWithAuthorization の成功は関係者が非ブロックリストであることを含意する。	対象	11
receiveWithAuthorization_not_blocklisted	theorem	Signatures	SignaturesTheorems.lean	receiveWithAuthorization の成功は関係者が非ブロックリストであることを含意する。	対象	11
permit_above_cap_allowlisted	theorem	Signatures	SignaturesTheorems.lean	上限超の額の permit 成功は owner が許可登録済みであることを含意する。	対象	11
transferWithAuthorization_above_cap_allowlisted	theorem	Signatures	SignaturesTheorems.lean	上限超の transferWithAuthorization 成功は payer(from) が許可登録済みであることを含意する。	対象	11
receiveWithAuthorization_above_cap_allowlisted	theorem	Signatures	SignaturesTheorems.lean	上限超の receiveWithAuthorization 成功は payer(from) が許可登録済みであることを含意する。	対象	11
permit_revert_noop	theorem	Signatures	SignaturesTheorems.lean	permit が revert した場合、状態は一切変化しない、という定理。	対象	10
transferWithAuthorization_revert_noop	theorem	Signatures	SignaturesTheorems.lean	transferWithAuthorization が revert した場合、状態は一切変化しない、という定理。	対象	10
receiveWithAuthorization_revert_noop	theorem	Signatures	SignaturesTheorems.lean	receiveWithAuthorization が revert した場合、状態は一切変化しない、という定理。	対象	10
cancelAuthorization_revert_noop	theorem	Signatures	SignaturesTheorems.lean	cancelAuthorization が revert した場合、状態は一切変化しない、という定理。	対象	9
instFintypeBitVec	instance	Foundation	State.lean	任意の BitVec が有限型であることを与えるインスタンス。総供給=Σ残高 の表現に必要。	対象	0
allowlistLimitAmount	def	Foundation	State.lean	V2 アローリストの上限額（100,000 × 1e18）。超過する送金は許可登録を要求する。	対象外	1
State	structure	Foundation	State.lean	FiatTokenV2 のストレージを継承チェーン全体にわたって写し取った状態構造体。	対象外	0
State.empty	def	Foundation	State.lean	全ゼロ・初期化前の状態。各不変条件が充足可能であることの正規の証人。	対象外	6
WF	structure	Foundation	State.lean	フラグ写像が 0/1 のみ・initializedVersion∈{0,1,2} を保証する健全性不変条件。	対象外	1
State.totalBalances	def	Foundation	State.lean	全口座残高の自然数としての総和。アドレス空間が有限なので well-defined。	対象外	3
SupplyConserved	def	Foundation	State.lean	totalSupply が全残高の総和に等しいという、中心となる監査不変条件。	対象	2
wf_empty	theorem	Foundation	State.lean	初期状態 State.empty が WF を満たす、という定理（WF の充足可能性）。	対象	5
supplyConserved_empty	theorem	Foundation	State.lean	初期状態 State.empty が SupplyConserved を満たす、という定理。	対象	5
State.setInitializedVersion	def	Upgradeability	Upgradeability.lean	initializedVersion を v に書き換える更新関数（0=未初期化, 1=V1, 2=V2）。	対象外	2
initializeResult	def	Upgradeability	Upgradeability.lean	initialize の直線的代入ブロック。各書き込みは別フィールドなので同時更新としてモデル化。	対象外	6
initializeV1	def	Upgradeability	Upgradeability.lean	initialize(...)（Lean キーワード回避で改名）：未初期化からのみ実行できる一回限りの初期化関数。	対象外	9
initializeV2	def	Upgradeability	Upgradeability.lean	initializeV2()：version 1 からのみ実行でき、ラッチを 2 に上げる V2 初期化関数。	対象外	6
authorizeUpgrade	def	Upgradeability	Upgradeability.lean	_authorizeUpgrade：onlyOwner ゲートだけを持つ空本体のアップグレード認可関数。	対象外	5
upgradeTo	def	Upgradeability	Upgradeability.lean	upgradeTo(newImplementation)：_authorizeUpgrade(onlyOwner) を通すアップグレード入口（slot 書き込みは対象外）。	対象外	5
upgradeToAndCall	def	Upgradeability	Upgradeability.lean	upgradeToAndCall(newImplementation,data)：upgradeTo に後続 delegatecall を加えた入口（slot/呼び出しは対象外）。	対象外	5
initializeV1_ok	theorem	Upgradeability	UpgradeabilityTheorems.lean	成功した initializeV1 を順方向に特徴づける補助補題。	対象外	11
initializeV1_requires_uninitialized	theorem	Upgradeability	UpgradeabilityTheorems.lean	initializeV1 は未初期化状態（version 0）からのみ成功する（二重実行ガード・順方向）。	対象	10
initializeV1_sets_version	theorem	Upgradeability	UpgradeabilityTheorems.lean	成功した initializeV1 はラッチを version 1 にする（効果）。	対象	10
initializeV1_already_initialized	theorem	Upgradeability	UpgradeabilityTheorems.lean	初期化済み状態（version≠0）からの initializeV1 は alreadyInitialized で revert する。	対象	11
initializeV1_not_reinitializable	theorem	Upgradeability	UpgradeabilityTheorems.lean	一度成功後、結果状態への 2 回目の initializeV1 は常に alreadyInitialized で revert する（再初期化不可）。	対象	9
initializeV1_wf	theorem	Upgradeability	UpgradeabilityTheorems.lean	initializeV1 は健全性不変条件 WF を保つ、という定理。	対象	12
initializeV1_conserves	theorem	Upgradeability	UpgradeabilityTheorems.lean	initializeV1 は供給保存不変条件 SupplyConserved を保つ、という定理。	対象	11
initializeV1_sets_owner	theorem	Upgradeability	UpgradeabilityTheorems.lean	initializeV1 は指定の owner とロールアドレス群を設定する（効果）。	対象	10
initializeV1_sets_minterAdmin	theorem	Upgradeability	UpgradeabilityTheorems.lean	成功した initializeV1 は minterAdmin を指定値に設定する（効果）。	対象	10
initializeV1_sets_pauser	theorem	Upgradeability	UpgradeabilityTheorems.lean	成功した initializeV1 は pauser を指定値に設定する（効果）。	対象	10
initializeV1_sets_blocklister	theorem	Upgradeability	UpgradeabilityTheorems.lean	成功した initializeV1 は blocklister を指定値に設定する（効果）。	対象	10
initializeV1_blocklists_self	theorem	Upgradeability	UpgradeabilityTheorems.lean	initializeV1 は自身のアドレスをブロックリスト登録する（blocklisted[address(this)]=1）（効果）。	対象	11
initializeV2_ok	theorem	Upgradeability	UpgradeabilityTheorems.lean	成功した initializeV2 を順方向に特徴づける補助補題。	対象外	7
initializeV2_requires_v1	theorem	Upgradeability	UpgradeabilityTheorems.lean	initializeV2 は version 1 からのみ成功する（二重実行ガード・順方向）。	対象	7
initializeV2_sets_version	theorem	Upgradeability	UpgradeabilityTheorems.lean	成功した initializeV2 はラッチを version 2 に上げる（効果）。	対象	7
initializeV2_wrong_version	theorem	Upgradeability	UpgradeabilityTheorems.lean	version 1 以外からの initializeV2 は revert する（二重実行ガード・revert形）。	対象	8
initializeV2_not_reinitializable	theorem	Upgradeability	UpgradeabilityTheorems.lean	一度成功後、2 回目の initializeV2 は常に revert する（ラッチが 2≠1）（再初期化不可）。	対象	8
initializeV2_locks_initializeV1	theorem	Upgradeability	UpgradeabilityTheorems.lean	initializeV2 成功後は V1 の initializeV1 も恒久的に締め出される（ラッチが 2≠0）。	対象	10
initializeV2_wf	theorem	Upgradeability	UpgradeabilityTheorems.lean	initializeV2 は健全性不変条件 WF を保つ、という定理。	対象	11
initializeV2_conserves	theorem	Upgradeability	UpgradeabilityTheorems.lean	initializeV2 は供給保存不変条件 SupplyConserved を保つ、という定理。	対象	8
authorizeUpgrade_auth	theorem	Upgradeability	UpgradeabilityTheorems.lean	_authorizeUpgrade は owner のときのみ成功する（権限）。	対象	6
authorizeUpgrade_unauthorized	theorem	Upgradeability	UpgradeabilityTheorems.lean	owner でない呼び出し元は _authorizeUpgrade で notOwner により拒否される（権限・revert形）。	対象	7
upgradeTo_ok	theorem	Upgradeability	UpgradeabilityTheorems.lean	成功した upgradeTo は owner が認可し、モデル状態を変えない（slot 書き込みは対象外）。	対象	6
upgradeTo_auth	theorem	Upgradeability	UpgradeabilityTheorems.lean	upgradeTo によるアップグレード認可は owner のみが行える（権限）。	対象	6
upgradeTo_unauthorized	theorem	Upgradeability	UpgradeabilityTheorems.lean	owner でない upgradeTo は notOwner で revert する（権限・revert形）。	対象	9
upgradeTo_wf	theorem	Upgradeability	UpgradeabilityTheorems.lean	upgradeTo は健全性不変条件 WF を保つ、という定理。	対象	7
upgradeTo_conserves	theorem	Upgradeability	UpgradeabilityTheorems.lean	upgradeTo は供給保存不変条件 SupplyConserved を保つ、という定理。	対象	7
upgradeToAndCall_ok	theorem	Upgradeability	UpgradeabilityTheorems.lean	成功した upgradeToAndCall は owner が認可し、モデル状態を変えない。	対象	6
upgradeToAndCall_auth	theorem	Upgradeability	UpgradeabilityTheorems.lean	upgradeToAndCall によるアップグレード認可は owner のみが行える（権限）。	対象	6
upgradeToAndCall_unauthorized	theorem	Upgradeability	UpgradeabilityTheorems.lean	owner でない upgradeToAndCall は notOwner で revert する（権限・revert形）。	対象	9
upgradeToAndCall_wf	theorem	Upgradeability	UpgradeabilityTheorems.lean	upgradeToAndCall は健全性不変条件 WF を保つ、という定理。	対象	7
upgradeToAndCall_conserves	theorem	Upgradeability	UpgradeabilityTheorems.lean	upgradeToAndCall は供給保存不変条件 SupplyConserved を保つ、という定理。	対象	7
initializeV1_revert_noop	theorem	Upgradeability	UpgradeabilityTheorems.lean	initializeV1 が revert した場合、状態は一切変化しない、という定理。	対象	8
initializeV2_revert_noop	theorem	Upgradeability	UpgradeabilityTheorems.lean	initializeV2 が revert した場合、状態は一切変化しない、という定理。	対象	6
upgradeTo_revert_noop	theorem	Upgradeability	UpgradeabilityTheorems.lean	upgradeTo が revert した場合、状態は一切変化しない、という定理。	対象	6
upgradeToAndCall_revert_noop	theorem	Upgradeability	UpgradeabilityTheorems.lean	upgradeToAndCall が revert した場合、状態は一切変化しない、という定理。	対象	6
U256	abbrev	Foundation	Word.lean	Solidity の uint256 を表す語型（BitVec 256）。	対象外	0
U8	abbrev	Foundation	Word.lean	Solidity の uint8 を表す語型（BitVec 8）。decimals や initializedVersion 用。	対象外	0
Bytes32	abbrev	Foundation	Word.lean	Solidity の bytes32 を表す語型。U256 と同一だが可読性のため別名で保持。	対象外	0
MAX_U256	def	Foundation	Word.lean	type(uint256).max = 2^256 − 1。transferFrom の無限承認分岐で使う定数。	対象外	1
MAX_U256_toNat	theorem	Foundation	Word.lean	MAX_U256 を自然数に直すと 2^256 − 1 になる、という補題。	対象外	1
add?	def	Foundation	Word.lean	Solidity 0.8 のチェック付き加算。和が 256 ビットに収まらなければ revert する。	対象外	2
sub?	def	Foundation	Word.lean	Solidity 0.8 のチェック付き減算。b > a なら revert する。	対象外	2
add?_of_lt	theorem	Foundation	Word.lean	和が 2^256 未満なら add? は成功して通常の和を返す、という補題。	対象	3
add?_eq_ok	theorem	Foundation	Word.lean	add? が成功したなら結果は通常の和であり桁あふれしていない、という補題。	対象	3
add?_toNat	theorem	Foundation	Word.lean	成功した add? は自然数加算と一致する（ラップアラウンドしない）、という補題。	対象	4
add?_comm	theorem	Foundation	Word.lean	add? は引数の順序に依らず可換である、という補題。	対象外	3
sub?_of_le	theorem	Foundation	Word.lean	b ≤ a なら sub? は成功して通常の差を返す、という補題。	対象	3
sub?_eq_ok	theorem	Foundation	Word.lean	sub? が成功したなら結果は通常の差であり桁借りしていない、という補題。	対象	3
sub?_toNat	theorem	Foundation	Word.lean	成功した sub? は自然数減算と一致する、という補題。	対象	4
sub?_self	theorem	Foundation	Word.lean	同じ値どうしの sub? は必ず 0 を返す、という補題。	対象外	3
add?_sub?_cancel	theorem	Foundation	Word.lean	a+b が c で成功するなら c−b は a に戻る、という往復（借方→貸方）補題。	対象	6
sub?_add?_cancel	theorem	Foundation	Word.lean	a−b が c で成功するなら c+b は a に戻る、という往復補題。	対象	6