JPYCv2 形式検証

外観

JPYC.add?_comm ​

名称・種別 ​

  • 名称: JPYC.add?_comm
  • 種別: theorem
  • モジュール: JpycFormalVerification.Word
  • ソース: JpycFormalVerification/Word.lean:60-63
  • 概要: add? は引数の順序に依らず可換である、という補題。
  • 仕様: 対象外

型シグネチャ ​

lean
∀ (a b : JPYC.U256), Eq (JPYC.add? a b) (JPYC.add? b a)

「add? a b = add? b a」という定理です。加算は左右を入れ替えても、成功・失敗も結果も変わりません（可換性）。

和訳 docstring ​

add? は可換である：a + b と b + a は、成功・失敗も結果も一致する。API の完全性のために用意したもので、証明の下流では使われていない。

解説 ​

何を述べているか。 add? は引数の順序によらない、という主張です。条件 和 < 2^256 も結果 a + b も左右対称だからです。

直感。 足し算の順序は結果を変えない、という当たり前の代数的性質です。

なぜ安全性に効くか。 証明の途中で引数を入れ替えて式を正規化するのに便利な API です。Nat.add_comm と BitVec.add_comm から従います。なお現状この補題は下流の証明では使われておらず、add? の代数的性質を補完する API 完全性 のために置いてあります。

図解 ​

Lean ソースコード ​

lean
/-- `add?` is commutative: `a + b` and `b + a` agree on both success/failure and
result. Provided for API completeness; it has no downstream use in the proofs. -/
theorem add?_comm (a b : U256) : add? a b = add? b a := by
  simp only [add?, Nat.add_comm a.toNat b.toNat, BitVec.add_comm a b]

依存 ​