Add LawfulBEq Uint256 instance to enable == reasoning in proofs

[Th0rgal]

Problem

Proofs that need to reason about Uint256 == comparisons are stuck: Uint256 lacks a LawfulBEq instance, so there is no lemma connecting BEq.beq to propositional = at reasoning time.

Uint256 is declared with deriving DecidableEq only (Verity/Core/Uint256.lean:24); it has no explicit BEq/LawfulBEq instance, so its BEq comes from the generic decidable-eq fallback with no lawfulness bridge.

By contrast, both sibling scalar types already carry explicit lawful instances:

• LawfulBEq Address — Verity/Core/Address.lean:56
• LawfulBEq Uint16 — Verity/Core/Uint16.lean:64 (sitting next to an explicit instance : BEq Uint16 := ⟨fun a b => decide (a = b)⟩)

Impact

Affects 4 of 5 contracts whose guard checks use require (value == 1) on Uint256-mapped storage — those == comparisons can't be discharged in proofs without the BEq.beq ↔ = bridge.

Unaffected:

• Address-based comparisons (via getStorageAddr) — covered by LawfulBEq Address.
• Literal decidability (decide) — independent of the missing instance.

Fix

Add to Verity/Core/Uint256.lean, matching the existing Uint16/Address pattern:

instance : LawfulBEq Uint256 where
  eq_of_beq {a b} h := by
    simp only [BEq.beq] at h
    exact of_decide_eq_true h
  rfl {a} := by
    show decide (a = a) = true
    exact decide_eq_true rfl

One instance; no axioms; mirrors the already-proven sibling instances.

Notes

No existing issue (open or closed) tracks this gap. Closest open issues are #1723 (extend proven fragment to full CompilationModel surface) and #1724 (Solidity feature parity), but neither names it.