ArithmeticProfile.lean

/-
  Compiler.Proofs.ArithmeticProfile: Arithmetic profile specification and proofs

  Documents and proves the arithmetic semantics used across all compilation
  layers. Verity uses wrapping modular arithmetic at 2^256, matching the
  EVM Yellow Paper specification.

  This file serves as the single formal reference for arithmetic behavior:
  - Proves wrapping is consistent across EDSL and compiler layers
  - Proves EVMYulLean bridge agreement for pure builtins
  - Documents the checked (safe) arithmetic alternative at EDSL level
  - Establishes that all backend profiles share identical arithmetic semantics

  Run: lake build Compiler.Proofs.ArithmeticProfile
-/

import Compiler.Constants
import Compiler.Proofs.YulGeneration.Builtins
import Compiler.Proofs.YulGeneration.Backends.EvmYulLeanAdapter
import Compiler.Proofs.YulGeneration.Backends.EvmYulLeanBridgeLemmas
import Verity.Core.Uint256
import EvmYul.UInt256

namespace Compiler.Proofs.ArithmeticProfile

open Compiler.Constants (evmModulus)
open Compiler.Proofs.YulGeneration (evalBuiltinCall)
open Compiler.Proofs.YulGeneration.Backends (evalPureBuiltinViaEvmYulLean)

-- ============================================================================
-- § 1. Arithmetic profile constants
-- ============================================================================

/-- The arithmetic modulus is 2^256, matching EVM word size. -/
theorem modulus_is_2_pow_256 : evmModulus = 2 ^ 256 := rfl

/-- EVMYulLean's UInt256.size equals Verity's evmModulus. -/
theorem evmyullean_size_eq_verity_modulus :
    EvmYul.UInt256.size = evmModulus := by decide

-- ============================================================================
-- § 2. Wrapping semantics: compiler builtins are total and wrapping
-- ============================================================================

-- Dummy state parameters (arithmetic builtins are state-independent).
private def s : Nat → Nat := fun _ => 0
private def sender : Nat := 0
private def sel : Nat := 0
private def cd : List Nat := []

/-- Addition wraps: (a + b) mod 2^256. -/
theorem add_wraps (a b : Nat) :
    evalBuiltinCall s sender sel cd "add" [a, b] = some ((a + b) % evmModulus) := by
  simp [evalBuiltinCall, Compiler.Proofs.YulGeneration.evalBuiltinCallWithContext]

/-- Subtraction wraps: (2^256 + a - b) mod 2^256. -/
theorem sub_wraps (a b : Nat) :
    evalBuiltinCall s sender sel cd "sub" [a, b] =
      some ((evmModulus + a % evmModulus - b % evmModulus) % evmModulus) := by
  simp [evalBuiltinCall, Compiler.Proofs.YulGeneration.evalBuiltinCallWithContext]

/-- Multiplication wraps: (a * b) mod 2^256. -/
theorem mul_wraps (a b : Nat) :
    evalBuiltinCall s sender sel cd "mul" [a, b] = some ((a * b) % evmModulus) := by
  simp [evalBuiltinCall, Compiler.Proofs.YulGeneration.evalBuiltinCallWithContext]

/-- Division by zero returns 0. -/
theorem div_by_zero (a : Nat) :
    evalBuiltinCall s sender sel cd "div" [a, 0] = some 0 := by
  simp [evalBuiltinCall, Compiler.Proofs.YulGeneration.evalBuiltinCallWithContext]

/-- Modulo by zero returns 0. -/
theorem mod_by_zero (a : Nat) :
    evalBuiltinCall s sender sel cd "mod" [a, 0] = some 0 := by
  simp [evalBuiltinCall, Compiler.Proofs.YulGeneration.evalBuiltinCallWithContext]

-- ============================================================================
-- § 3. EVMYulLean bridge agreement for pure arithmetic
-- ============================================================================

-- Arithmetic bridging is now universally proved for add/sub/mul/div/mod.
-- Bitwise `and`/`or`/`xor` plus the shift family now also have direct symbolic bridge lemmas.
-- `not` still retains concrete bridge coverage here.

/-- Universal bridge theorem for addition. -/
theorem add_bridge (a b : Nat) :
    evalBuiltinCall s sender sel cd "add" [a, b] =
      evalPureBuiltinViaEvmYulLean "add" [a, b] := by
  exact Compiler.Proofs.YulGeneration.Backends.evalBuiltinCall_add_bridge
    s sender sel cd a b

/-- Universal bridge theorem for subtraction. -/
theorem sub_bridge (a b : Nat) :
    evalBuiltinCall s sender sel cd "sub" [a, b] =
      evalPureBuiltinViaEvmYulLean "sub" [a, b] := by
  exact Compiler.Proofs.YulGeneration.Backends.evalBuiltinCall_sub_bridge
    s sender sel cd a b

/-- Universal bridge theorem for multiplication. -/
theorem mul_bridge (a b : Nat) :
    evalBuiltinCall s sender sel cd "mul" [a, b] =
      evalPureBuiltinViaEvmYulLean "mul" [a, b] := by
  exact Compiler.Proofs.YulGeneration.Backends.evalBuiltinCall_mul_bridge
    s sender sel cd a b

/-- Universal bridge theorem for division. -/
theorem div_bridge (a b : Nat) :
    evalBuiltinCall s sender sel cd "div" [a, b] =
      evalPureBuiltinViaEvmYulLean "div" [a, b] := by
  exact Compiler.Proofs.YulGeneration.Backends.evalBuiltinCall_div_bridge
    s sender sel cd a b

/-- Universal bridge theorem for modulo. -/
theorem mod_bridge (a b : Nat) :
    evalBuiltinCall s sender sel cd "mod" [a, b] =
      evalPureBuiltinViaEvmYulLean "mod" [a, b] := by
  exact Compiler.Proofs.YulGeneration.Backends.evalBuiltinCall_mod_bridge
    s sender sel cd a b

/-- Universal bridge theorem for bitwise and. -/
theorem and_bridge (a b : Nat) :
    evalBuiltinCall s sender sel cd "and" [a, b] =
      evalPureBuiltinViaEvmYulLean "and" [a, b] := by
  exact Compiler.Proofs.YulGeneration.Backends.evalBuiltinCall_and_bridge
    s sender sel cd a b

/-- Universal bridge theorem for bitwise or. -/
theorem or_bridge (a b : Nat) :
    evalBuiltinCall s sender sel cd "or" [a, b] =
      evalPureBuiltinViaEvmYulLean "or" [a, b] := by
  exact Compiler.Proofs.YulGeneration.Backends.evalBuiltinCall_or_bridge
    s sender sel cd a b

/-- Universal bridge theorem for bitwise xor. -/
theorem xor_bridge (a b : Nat) :
    evalBuiltinCall s sender sel cd "xor" [a, b] =
      evalPureBuiltinViaEvmYulLean "xor" [a, b] := by
  exact Compiler.Proofs.YulGeneration.Backends.evalBuiltinCall_xor_bridge
    s sender sel cd a b

/-- Universal bridge theorem for shift-left. -/
theorem shl_bridge (shift value : Nat) :
    evalBuiltinCall s sender sel cd "shl" [shift, value] =
      evalPureBuiltinViaEvmYulLean "shl" [shift, value] := by
  exact Compiler.Proofs.YulGeneration.Backends.evalBuiltinCall_shl_bridge
    s sender sel cd shift value

/-- Universal bridge theorem for shift-right. -/
theorem shr_bridge (shift value : Nat) :
    evalBuiltinCall s sender sel cd "shr" [shift, value] =
      evalPureBuiltinViaEvmYulLean "shr" [shift, value] := by
  exact Compiler.Proofs.YulGeneration.Backends.evalBuiltinCall_shr_bridge
    s sender sel cd shift value

-- ============================================================================
-- § 4. Backend profile invariant
-- ============================================================================

-- All backend profiles (semantic, solidity-parity-ordering, solidity-parity)
-- use the same evalBuiltinCall function. The profiles differ only in Yul
-- output shape (selector sorting, patch pass enablement), not arithmetic
-- semantics. This is enforced structurally: there is a single evalBuiltinCall
-- definition that all codepaths use.

/-- The BuiltinBackend enum has exactly two variants. -/
example : ∀ b : Compiler.Proofs.YulGeneration.BuiltinBackend,
    b = .verity ∨ b = .evmYulLean := by
  intro b; cases b <;> simp

-- ============================================================================
-- § 5. Scope boundaries (what is NOT proved here)
-- ============================================================================

-- Gas semantics: not formally modeled. Proofs establish semantic correctness
-- (same result), not gas correctness (same cost or bounded cost).
--
-- Compiler-layer overflow detection: the compiler does not insert automatic
-- overflow checks. Contracts that need checked arithmetic must use the EDSL
-- safeAdd/safeSub/safeMul functions, which return Option and revert on None.
--
-- Cryptographic primitives: keccak256 is axiomatized (see AXIOMS.md).
-- The mapping-slot derivation trusts the keccak FFI.
--
-- Universal bridge equivalence: all pure arithmetic/comparison builtins plus
-- bitwise and/or/xor and the shift family now have direct symbolic bridge lemmas
-- in `Backends/EvmYulLeanBridgeLemmas.lean`.
-- `not` still relies on concrete bridge coverage.

end Compiler.Proofs.ArithmeticProfile