smartcontracts/FuzzProof.lean

## FuzzProof.lean
import Mathlib

namespace FuzzEquivalence

/-!
# Equivalence proof for the OptimismPortal2 fuzz test fix

File: packages/contracts-bedrock/test/L1/OptimismPortal2.t.sol:2614
Test: OptimismPortal2_Params_Test::testFuzz_params_validValues_succeeds

## Problem

The test uses `vm.assume (r / e * e = r)` to filter for inputs where
`_maxResourceLimit` is divisible by `_elasticityMultiplier`. With `e` uniform
in [1,255] this rejects ~97.6% of inputs, exhausting Foundry's 65536-rejection
limit.

## Fix

Replace the `vm.assume` with rounding by construction:
  `_maxResourceLimit := _maxResourceLimit / _elasticityMultiplier * _elasticityMultiplier`

BUT: `_gasLimit` and `_prevBoughtGas` are bounded from `_maxResourceLimit` BEFORE
`_elasticityMultiplier` is bounded (they appear earlier in the bound block). So
the fix requires reordering: move `_elasticityMultiplier` binding first, then
round `_maxResourceLimit`, then re-bound `_gasLimit` and `_prevBoughtGas`.

## What we prove

1. **Core lemmas**: rounding is sound (produces divisible values) and complete
   (divisible values are fixed points).
2. **Naive fix is unsound**: rounding in-place without re-bounding `_gasLimit`
   breaks the invariant `_gasLimit ≤ _maxResourceLimit`.
3. **Correct fix is equivalent**: the reordered version reaches exactly the same
   set of `TestState` values as the original `vm.assume` path.

## Scope

`TestState` models the four-variable submodel {r, e, g, b} only. The proof
establishes support-set equality (same states reachable), not distributional
equivalence. The gas burn equivalence is proved separately in `GasBurnEquivalence`.
-/

-- ---------------------------------------------------------------------------
-- 1. Core arithmetic lemmas
-- ---------------------------------------------------------------------------

/-- Rounding `r` down to the nearest multiple of `e` yields a result
    divisible by `e`. Holds unconditionally (ℕ: r / 0 = 0, n % 0 = n). -/
lemma rounded_mod_zero (r e : ℕ) : (r / e * e) % e = 0 := by
  rw [Nat.mul_comm]; exact Nat.mul_mod_right e (r / e)

/-- A value already divisible by `e` is unchanged by rounding. -/
lemma fixpoint_of_mod_zero (r e : ℕ) (h : r % e = 0) : r / e * e = r :=
  Nat.div_mul_cancel (Nat.dvd_of_mod_eq_zero h)

-- ---------------------------------------------------------------------------
-- 2. State model and invariants
-- ---------------------------------------------------------------------------

/-- The four values that reach the test body. -/
structure TestState where
  r : ℕ   -- _maxResourceLimit
  e : ℕ   -- _elasticityMultiplier
  g : ℕ   -- local _gasLimit
  b : ℕ   -- _prevBoughtGas

/-- Structural parameter relationships required for the fuzz harness inputs to be valid.
    This captures the four-variable submodel {r, e, g, b} only — not full contract
    invariants (base fee bounds, systemTxMaxGas interaction, etc.). -/
def Inv (s : TestState) (sysGas : ℕ) : Prop :=
  21000 ≤ s.r ∧ s.r ≤ sysGas ∧ 0 < s.e ∧ s.r % s.e = 0 ∧
  21000 ≤ s.g ∧ s.g ≤ s.r ∧ s.b ≤ s.r - s.g

-- ---------------------------------------------------------------------------
-- 3. Naive fix — round r in-place AFTER g and b are computed (WRONG)
--
-- This is what happens if you just replace vm.assume with rounding without
-- also re-bounding _gasLimit and _prevBoughtGas.
-- ---------------------------------------------------------------------------

def naiveFix (r g b e : ℕ) : TestState := ⟨r / e * e, e, g, b⟩

/-- Counterexample: r = 21300, e = 200, g = 21250.
      21300 / 200 = 106   (integer division)
      r_rounded = 106 × 200 = 21200
      g = 21250 > 21200 = r_rounded    ← Inv.g_ceil violated
    Note: e = 200 is within the uint8 range [1, 255] used in the real test.
    The `21000 ≤ r / e * e` condition confirms the failure is the g > r_rounded
    violation, not the floor-below-21000 case. -/
theorem naive_fix_not_sound :
    ∃ r g b e sysGas : ℕ,
    (21000 ≤ r ∧ r ≤ sysGas) ∧ (21000 ≤ g ∧ g ≤ r) ∧ b ≤ r - g ∧
    1 ≤ e ∧ 21000 ≤ r / e * e ∧
    ¬ (naiveFix r g b e).g ≤ (naiveFix r g b e).r :=
  ⟨21300, 21250, 0, 200, 30000,
    ⟨by norm_num, by norm_num⟩,
    ⟨by norm_num, by norm_num⟩,
    by norm_num,
    by norm_num,
    by norm_num,
    by decide⟩

-- ---------------------------------------------------------------------------
-- 4. Correct fix — reorder, round, then re-bound g and b
--
-- Required reordering of the bound block:
--   e   := bound(e_raw, 1,    255)           ← MOVED FIRST
--   r'  := bound(r_raw, 21000, sysGas)
--   r   := r' / e * e                        ← ROUNDED immediately
--   vm.assume(r ≥ 21000)
--   g   := bound(g_raw, 21000, r)            ← re-bounded from rounded r
--   b   := bound(b_raw, 0,    r - g)         ← re-bounded from rounded r
-- ---------------------------------------------------------------------------

theorem correct_fix_satisfies_inv
    {r_pre g b e sysGas : ℕ}
    (hpre : 21000 ≤ r_pre ∧ r_pre ≤ sysGas)
    (he   : 1 ≤ e)
    (hfl  : 21000 ≤ r_pre / e * e)
    (hg   : 21000 ≤ g ∧ g ≤ r_pre / e * e)
    (hb   : b ≤ r_pre / e * e - g) :
    Inv ⟨r_pre / e * e, e, g, b⟩ sysGas := by
  unfold Inv
  exact ⟨hfl, le_trans (Nat.div_mul_le_self r_pre e) hpre.2, he,
         rounded_mod_zero r_pre e, hg.1, hg.2, hb⟩

-- ---------------------------------------------------------------------------
-- 5. Equivalence — the two paths reach exactly the same set of states
-- ---------------------------------------------------------------------------

/-- Forward: every state reachable by path1 is also reachable by the correct
    fix.  Witness: r_pre = r.  Since r % e = 0, rounding is the identity
    (fixpoint_of_mod_zero), so the resulting state is unchanged. -/
theorem path1_to_correct_fix
    {r g b e sysGas : ℕ}
    (hr : 21000 ≤ r ∧ r ≤ sysGas) (hg : 21000 ≤ g ∧ g ≤ r)
    (hb : b ≤ r - g) (he : 1 ≤ e) (hdv : r % e = 0) :
    ∃ r_pre : ℕ,
      (21000 ≤ r_pre ∧ r_pre ≤ sysGas) ∧ 1 ≤ e ∧
      21000 ≤ r_pre / e * e ∧
      (21000 ≤ g ∧ g ≤ r_pre / e * e) ∧
      b ≤ r_pre / e * e - g ∧
      (⟨r_pre / e * e, e, g, b⟩ : TestState) = ⟨r, e, g, b⟩ := by
  have hfix : r / e * e = r := fixpoint_of_mod_zero r e hdv
  refine ⟨r, hr, he, ?_, ?_, ?_, ?_⟩ <;> simp only [hfix]
  · exact hr.1
  · exact hg
  · exact hb

/-- Backward: every state reachable by the correct fix satisfies path1's
    invariants.  The divisibility invariant holds by rounded_mod_zero;
    g and b bounds hold because they were re-bounded from the rounded r. -/
theorem correct_fix_to_path1
    {r_pre g b e sysGas : ℕ}
    (hpre : 21000 ≤ r_pre ∧ r_pre ≤ sysGas)
    (he   : 1 ≤ e)
    (hfl  : 21000 ≤ r_pre / e * e)
    (hg   : 21000 ≤ g ∧ g ≤ r_pre / e * e)
    (hb   : b ≤ r_pre / e * e - g) :
    ∃ r : ℕ,
      (21000 ≤ r ∧ r ≤ sysGas) ∧ (21000 ≤ g ∧ g ≤ r) ∧ b ≤ r - g ∧
      1 ≤ e ∧ r % e = 0 ∧
      (⟨r, e, g, b⟩ : TestState) = ⟨r_pre / e * e, e, g, b⟩ :=
  ⟨r_pre / e * e,
   ⟨hfl, le_trans (Nat.div_mul_le_self r_pre e) hpre.2⟩,
   hg, hb, he,
   rounded_mod_zero r_pre e,
   rfl⟩

/-- Main theorem: the set of TestState values reachable by path1 equals the
    set reachable by the correct fix. -/
theorem paths_equivalent (sysGas : ℕ) :
    {s : TestState | ∃ r g b e,
        (21000 ≤ r ∧ r ≤ sysGas) ∧ (21000 ≤ g ∧ g ≤ r) ∧ b ≤ r - g ∧
        1 ≤ e ∧ r % e = 0 ∧ s = ⟨r, e, g, b⟩} =
    {s : TestState | ∃ r_pre g b e,
        (21000 ≤ r_pre ∧ r_pre ≤ sysGas) ∧ 1 ≤ e ∧
        21000 ≤ r_pre / e * e ∧
        (21000 ≤ g ∧ g ≤ r_pre / e * e) ∧
        b ≤ r_pre / e * e - g ∧
        s = ⟨r_pre / e * e, e, g, b⟩} := by
  ext s
  simp only [Set.mem_setOf_eq]
  constructor
  · rintro ⟨r, g, b, e, hr, hg, hb, he, hdv, rfl⟩
    obtain ⟨r_pre, hpre, he', hfl, hg', hb', heq⟩ :=
      path1_to_correct_fix hr hg hb he hdv
    exact ⟨r_pre, g, b, e, hpre, he', hfl, hg', hb', heq.symm⟩
  · rintro ⟨r_pre, g, b, e, hpre, he, hfl, hg, hb, rfl⟩
    obtain ⟨r, hr, hg', hb', he', hdv, heq⟩ :=
      correct_fix_to_path1 hpre he hfl hg hb
    exact ⟨r, g, b, e, hr, hg', hb', he', hdv, heq.symm⟩

-- ---------------------------------------------------------------------------
-- 6. Axiom check and sanity tests
-- ---------------------------------------------------------------------------

-- Confirm proof depends only on standard axioms (no sorry)
#print axioms paths_equivalent
#print axioms naive_fix_not_sound

-- Concrete sanity checks (kernel-verified via decide)
#guard (21500 / 700 * 700 : Nat) = 21000   -- rounding drops to 21000
#guard (21000 / 255 * 255 : Nat) = 20910   -- below 21000 → vm.assume fires
#guard (21000 / 1   * 1   : Nat) = 21000   -- e=1 always rounds cleanly
#guard (65536 / 256 * 256 : Nat) = 65536   -- power-of-2 case

end FuzzEquivalence

-- =============================================================================
-- Gas Burn Equivalence
-- =============================================================================
--
-- Proves that replacing:
--   vm.assume(_prevBaseFee * maxPercentIncrease * _gasLimit / 100 < MAX_GAS_LIMIT * 4 / 5)
-- with a direct bound on _prevBaseFee:
--   gasBurnDenom := maxPercentIncrease * gasLimit
--   gasBurnCap   := (MAX_GAS_LIMIT * 4/5 * 100 - 1) / gasBurnDenom   (or 3 gwei if denom = 0)
--   _prevBaseFee  := bound(_prevBaseFee, 0, min(3 gwei, gasBurnCap))
-- yields exactly the same set of reachable prevBaseFee values (modulo the
-- acknowledged lower-bound change from 1 to 0).
--
-- File: packages/contracts-bedrock/test/L1/OptimismPortal2.t.sol:2664 (original)
-- =============================================================================

namespace GasBurnEquivalence

/-- Core arithmetic lemma: p * m < K ↔ p ≤ (K - 1) / m, for m > 0 and K > 0.
    Forward: p * m < K → p * m ≤ K - 1 → p ≤ (K-1)/m (Euclidean floor).
    Backward: p ≤ (K-1)/m → p*m ≤ (K-1)/m*m ≤ K-1 < K. -/
lemma mul_lt_iff_le_pred_div (p m K : ℕ) (hm : 0 < m) (hK : 0 < K) :
    p * m < K ↔ p ≤ (K - 1) / m := by
  constructor
  · intro h
    by_contra hlt
    push_neg at hlt
    have hmod   := Nat.div_add_mod (K - 1) m
    rw [Nat.mul_comm m ((K - 1) / m)] at hmod
    -- hmod : (K - 1) / m * m + (K - 1) % m = K - 1
    have hmodlt := Nat.mod_lt (K - 1) hm
    have hmul : (K - 1) / m * m + m ≤ p * m := by
      have h1 : ((K - 1) / m + 1) * m ≤ p * m := Nat.mul_le_mul_right m hlt
      linarith [show ((K - 1) / m + 1) * m = (K - 1) / m * m + m from by ring]
    -- K - 1 uses saturating subtraction; omega handles K = (K-1) + 1 via hK
    have hK1 : K - 1 + 1 = K := by omega
    linarith
  · intro h
    have h1 := Nat.mul_le_mul_right m h
    have h2 := Nat.div_mul_le_self (K - 1) m
    omega

/-- The gas burn condition `p * m / 100 < T` is equivalent to `p ≤ (100 * T - 1) / m`
    when m > 0 and T > 0.
    In the test: p = _prevBaseFee, m = maxPercentIncrease * _gasLimit,
    T = MAX_GAS_LIMIT * 4 / 5 = 24_000_000.
    Note: the proof's LHS set includes p = 0, whereas the original test bounded
    _prevBaseFee from 1. This is an acknowledged semantic change. -/
lemma gas_burn_iff_bound (p m T : ℕ) (hm : 0 < m) (hT : 0 < T) :
    p * m / 100 < T ↔ p ≤ (100 * T - 1) / m := by
  -- n / 100 < T ↔ n < 100 * T  (Nat.div_lt_iff_lt_mul with k = 100)
  have hdiv : p * m / 100 < T ↔ p * m < 100 * T := by omega
  rw [hdiv]
  exact mul_lt_iff_le_pred_div p m (100 * T) hm (by omega)

/-- Main theorem: the set of prevBaseFee values satisfying the original vm.assume
    equals the set reachable by the direct bound.  For m = 0 (maxPercentIncrease = 0
    or gasLimit = 0), the gas burn is always 0 < T so no cap is needed (cap = P). -/
theorem gas_burn_paths_equivalent (P T : ℕ) (hT : 0 < T) (m : ℕ) :
    {p : ℕ | p ≤ P ∧ p * m / 100 < T} =
    {p : ℕ | p ≤ if m = 0 then P else min P ((100 * T - 1) / m)} := by
  ext p
  simp only [Set.mem_setOf_eq]
  by_cases hm : m = 0
  · subst hm; simp [hT]
  · have hm' : 0 < m := Nat.pos_of_ne_zero hm
    simp only [hm, ↓reduceIte, Nat.le_min, gas_burn_iff_bound p m T hm' hT]

-- Confirm no sorry
#print axioms gas_burn_paths_equivalent

-- Concrete sanity checks with realistic test values (kernel-verified via decide):
-- maxPercentIncrease = 100, gasLimit = 21000 → m = 100 * 21000 = 2_100_000
-- T = MAX_GAS_LIMIT * 4 / 5 = 30_000_000 * 4 / 5 = 24_000_000
-- cap = (100 * 24_000_000 - 1) / 2_100_000 = 2_399_999_999 / 2_100_000 = 1142
#guard (100 * (30_000_000 * 4 / 5) - 1) / (100 * 21000) = 1142

-- Verify: cap satisfies condition (cap * m / 100 < T)
#guard (1142 * 2100000 / 100 : Nat) = 23982000   -- 23982000 < 24000000 ✓

-- Verify: cap + 1 violates condition
#guard (1143 * 2100000 / 100 : Nat) = 24003000   -- 24003000 ≥ 24000000 ✓

-- Edge: m = 0 (maxPercentIncrease = 0), gas burn is always 0 < T
#guard (999 * 0 / 100 : Nat) = 0                 -- 0 < any T ✓

end GasBurnEquivalence

## gist-readme.md

      
    Raw
  

              gist-readme.md
            
          
    FuzzProof.lean — Formal correctness proof for OptimismPortal2 fuzz test fix

This Lean 4 / Mathlib proof verifies that two changes to
testFuzz_params_validValues_succeeds in OptimismPortal2.t.sol preserve
the set of reachable test states exactly.
Background

The test was exhausting Foundry's 65,536-rejection limit because two
vm.assume filters were rejecting the vast majority of inputs:


vm.assume((_maxResourceLimit / _elasticityMultiplier) * _elasticityMultiplier == _maxResourceLimit)
— requires divisibility; with _elasticityMultiplier uniform in [1,255] this
rejects ~97.6% of inputs.


vm.assume(_prevBaseFee * maxPercentIncrease * _gasLimit / 100 < MAX_GAS_LIMIT * 4 / 5)
— a gas-burn safety condition; can reject many inputs depending on parameter ranges.


What we prove

FuzzEquivalence (namespace)

paths_equivalent: The set of TestState values {r, e, g, b} reachable
via the original vm.assume divisibility filter equals the set reachable via
the rounding fix (r := r / e * e), provided _gasLimit and _prevBoughtGas
are re-bounded from the rounded r.
The key insight is that every r satisfying r % e = 0 is a fixed point of
rounding (r / e * e = r), and every rounded value r_pre / e * e is divisible
by e. So the two parameter-space descriptions are identical.
naive_fix_not_sound: A concrete counterexample showing that rounding
_maxResourceLimit in-place without re-bounding _gasLimit and
_prevBoughtGas breaks the invariant _gasLimit ≤ _maxResourceLimit.
(Witness: r=21300, e=200, g=21250 → rounded r=21200 < g.)
GasBurnEquivalence (namespace)

gas_burn_paths_equivalent: The set of _prevBaseFee values satisfying
_prevBaseFee * m / 100 < T (where m = maxPercentIncrease * gasLimit) equals
the set satisfying _prevBaseFee ≤ (100 * T - 1) / m (for m > 0).
This lets us replace the vm.assume with a direct bound(...) call using
the tight cap (100 * T - 1) / m, eliminating rejections entirely.
Axioms

Both main theorems depend only on standard Lean axioms:

propext — propositional extensionality
Classical.choice — classical choice (for gas_burn_paths_equivalent only)
Quot.sound — quotient soundness

No sorry.  Verified with #print axioms.
How to run

Prerequisites

Install elan (the Lean toolchain manager):
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
Setup

mkdir fuzz-proof && cd fuzz-proof
cat > lakefile.toml << 'LAKE'
name = "FuzzProof"
version = "0.1.0"
defaultTargets = ["FuzzProof"]

[[lean_lib]]
name = "FuzzProof"

[[require]]
name = "mathlib"
scope = "leanprover-community"
rev = "v4.28.0"
LAKE

# Pin the Lean version
echo 'leanprover/lean4:v4.28.0' > lean-toolchain

# Copy the proof file into place
cp FuzzProof.lean .
Build

lake update   # downloads Mathlib (first time: ~5 min)
lake build    # compiles the proof (first time: ~10 min for Mathlib cache)
A successful build prints no errors and ends with:
Build completed successfully (N jobs).

The #print axioms lines in the file confirm:
info: 'FuzzEquivalence.paths_equivalent' depends on axioms: [propext, Quot.sound]
info: 'GasBurnEquivalence.gas_burn_paths_equivalent' depends on axioms: [propext, Classical.choice, Quot.sound]

Quick check with Lean's pre-built Mathlib cache

lake exe cache get   # pulls pre-compiled Mathlib oleans (~2 GB download, saves recompilation)
lake build
Scope and limitations


The proof models {_maxResourceLimit, _elasticityMultiplier, _gasLimit, _prevBoughtGas}
as unbounded natural numbers (ℕ). The actual Solidity test uses uint32/uint64/uint128.
Overflow is out of scope (inputs are bounded well below overflow by the bound(...) calls).


TestState captures only the four-variable submodel. Other invariants (base fee
bounds, systemTxMaxGas interaction, etc.) are not modelled.


The proof establishes support-set equality (same set of states reachable),
not distributional equivalence (same probability distribution over states).
The fix changes the sampling distribution but not the coverage.
	import Mathlib

	namespace FuzzEquivalence

	/-!
	# Equivalence proof for the OptimismPortal2 fuzz test fix

	File: packages/contracts-bedrock/test/L1/OptimismPortal2.t.sol:2614
	Test: OptimismPortal2_Params_Test::testFuzz_params_validValues_succeeds

	## Problem

	The test uses `vm.assume (r / e * e = r)` to filter for inputs where
	`_maxResourceLimit` is divisible by `_elasticityMultiplier`. With `e` uniform
	in [1,255] this rejects ~97.6% of inputs, exhausting Foundry's 65536-rejection
	limit.

	## Fix

	Replace the `vm.assume` with rounding by construction:
	`_maxResourceLimit := _maxResourceLimit / _elasticityMultiplier * _elasticityMultiplier`

	BUT: `_gasLimit` and `_prevBoughtGas` are bounded from `_maxResourceLimit` BEFORE
	`_elasticityMultiplier` is bounded (they appear earlier in the bound block). So
	the fix requires reordering: move `_elasticityMultiplier` binding first, then
	round `_maxResourceLimit`, then re-bound `_gasLimit` and `_prevBoughtGas`.

	## What we prove

	1. Core lemmas: rounding is sound (produces divisible values) and complete
	(divisible values are fixed points).
	2. Naive fix is unsound: rounding in-place without re-bounding `_gasLimit`
	breaks the invariant `_gasLimit ≤ _maxResourceLimit`.
	3. Correct fix is equivalent: the reordered version reaches exactly the same
	set of `TestState` values as the original `vm.assume` path.

	## Scope

	`TestState` models the four-variable submodel {r, e, g, b} only. The proof
	establishes support-set equality (same states reachable), not distributional
	equivalence. The gas burn equivalence is proved separately in `GasBurnEquivalence`.
	-/

	-- ---------------------------------------------------------------------------
	-- 1. Core arithmetic lemmas
	-- ---------------------------------------------------------------------------

	/-- Rounding `r` down to the nearest multiple of `e` yields a result
	divisible by `e`. Holds unconditionally (ℕ: r / 0 = 0, n % 0 = n). -/
	lemma rounded_mod_zero (r e : ℕ) : (r / e * e) % e = 0 := by
	rw [Nat.mul_comm]; exact Nat.mul_mod_right e (r / e)

	/-- A value already divisible by `e` is unchanged by rounding. -/
	lemma fixpoint_of_mod_zero (r e : ℕ) (h : r % e = 0) : r / e * e = r :=
	Nat.div_mul_cancel (Nat.dvd_of_mod_eq_zero h)

	-- ---------------------------------------------------------------------------
	-- 2. State model and invariants
	-- ---------------------------------------------------------------------------

	/-- The four values that reach the test body. -/
	structure TestState where
	r : ℕ -- _maxResourceLimit
	e : ℕ -- _elasticityMultiplier
	g : ℕ -- local _gasLimit
	b : ℕ -- _prevBoughtGas

	/-- Structural parameter relationships required for the fuzz harness inputs to be valid.
	This captures the four-variable submodel {r, e, g, b} only — not full contract
	invariants (base fee bounds, systemTxMaxGas interaction, etc.). -/
	def Inv (s : TestState) (sysGas : ℕ) : Prop :=
	21000 ≤ s.r ∧ s.r ≤ sysGas ∧ 0 < s.e ∧ s.r % s.e = 0 ∧
	21000 ≤ s.g ∧ s.g ≤ s.r ∧ s.b ≤ s.r - s.g

	-- ---------------------------------------------------------------------------
	-- 3. Naive fix — round r in-place AFTER g and b are computed (WRONG)
	--
	-- This is what happens if you just replace vm.assume with rounding without
	-- also re-bounding _gasLimit and _prevBoughtGas.
	-- ---------------------------------------------------------------------------

	def naiveFix (r g b e : ℕ) : TestState := ⟨r / e * e, e, g, b⟩

	/-- Counterexample: r = 21300, e = 200, g = 21250.
	21300 / 200 = 106 (integer division)
	r_rounded = 106 × 200 = 21200
	g = 21250 > 21200 = r_rounded ← Inv.g_ceil violated
	Note: e = 200 is within the uint8 range [1, 255] used in the real test.
	The `21000 ≤ r / e * e` condition confirms the failure is the g > r_rounded
	violation, not the floor-below-21000 case. -/
	theorem naive_fix_not_sound :
	∃ r g b e sysGas : ℕ,
	(21000 ≤ r ∧ r ≤ sysGas) ∧ (21000 ≤ g ∧ g ≤ r) ∧ b ≤ r - g ∧
	1 ≤ e ∧ 21000 ≤ r / e * e ∧
	¬ (naiveFix r g b e).g ≤ (naiveFix r g b e).r :=
	⟨21300, 21250, 0, 200, 30000,
	⟨by norm_num, by norm_num⟩,
	⟨by norm_num, by norm_num⟩,
	by norm_num,
	by norm_num,
	by norm_num,
	by decide⟩

	-- ---------------------------------------------------------------------------
	-- 4. Correct fix — reorder, round, then re-bound g and b
	--
	-- Required reordering of the bound block:
	-- e := bound(e_raw, 1, 255) ← MOVED FIRST
	-- r' := bound(r_raw, 21000, sysGas)
	-- r := r' / e * e ← ROUNDED immediately
	-- vm.assume(r ≥ 21000)
	-- g := bound(g_raw, 21000, r) ← re-bounded from rounded r
	-- b := bound(b_raw, 0, r - g) ← re-bounded from rounded r
	-- ---------------------------------------------------------------------------

	theorem correct_fix_satisfies_inv
	{r_pre g b e sysGas : ℕ}
	(hpre : 21000 ≤ r_pre ∧ r_pre ≤ sysGas)
	(he : 1 ≤ e)
	(hfl : 21000 ≤ r_pre / e * e)
	(hg : 21000 ≤ g ∧ g ≤ r_pre / e * e)
	(hb : b ≤ r_pre / e * e - g) :
	Inv ⟨r_pre / e * e, e, g, b⟩ sysGas := by
	unfold Inv
	exact ⟨hfl, le_trans (Nat.div_mul_le_self r_pre e) hpre.2, he,
	rounded_mod_zero r_pre e, hg.1, hg.2, hb⟩

	-- ---------------------------------------------------------------------------
	-- 5. Equivalence — the two paths reach exactly the same set of states
	-- ---------------------------------------------------------------------------

	/-- Forward: every state reachable by path1 is also reachable by the correct
	fix. Witness: r_pre = r. Since r % e = 0, rounding is the identity
	(fixpoint_of_mod_zero), so the resulting state is unchanged. -/
	theorem path1_to_correct_fix
	{r g b e sysGas : ℕ}
	(hr : 21000 ≤ r ∧ r ≤ sysGas) (hg : 21000 ≤ g ∧ g ≤ r)
	(hb : b ≤ r - g) (he : 1 ≤ e) (hdv : r % e = 0) :
	∃ r_pre : ℕ,
	(21000 ≤ r_pre ∧ r_pre ≤ sysGas) ∧ 1 ≤ e ∧
	21000 ≤ r_pre / e * e ∧
	(21000 ≤ g ∧ g ≤ r_pre / e * e) ∧
	b ≤ r_pre / e * e - g ∧
	(⟨r_pre / e * e, e, g, b⟩ : TestState) = ⟨r, e, g, b⟩ := by
	have hfix : r / e * e = r := fixpoint_of_mod_zero r e hdv
	refine ⟨r, hr, he, ?_, ?_, ?_, ?_⟩ <;> simp only [hfix]
	· exact hr.1
	· exact hg
	· exact hb

	/-- Backward: every state reachable by the correct fix satisfies path1's
	invariants. The divisibility invariant holds by rounded_mod_zero;
	g and b bounds hold because they were re-bounded from the rounded r. -/
	theorem correct_fix_to_path1
	{r_pre g b e sysGas : ℕ}
	(hpre : 21000 ≤ r_pre ∧ r_pre ≤ sysGas)
	(he : 1 ≤ e)
	(hfl : 21000 ≤ r_pre / e * e)
	(hg : 21000 ≤ g ∧ g ≤ r_pre / e * e)
	(hb : b ≤ r_pre / e * e - g) :
	∃ r : ℕ,
	(21000 ≤ r ∧ r ≤ sysGas) ∧ (21000 ≤ g ∧ g ≤ r) ∧ b ≤ r - g ∧
	1 ≤ e ∧ r % e = 0 ∧
	(⟨r, e, g, b⟩ : TestState) = ⟨r_pre / e * e, e, g, b⟩ :=
	⟨r_pre / e * e,
	⟨hfl, le_trans (Nat.div_mul_le_self r_pre e) hpre.2⟩,
	hg, hb, he,
	rounded_mod_zero r_pre e,
	rfl⟩

	/-- Main theorem: the set of TestState values reachable by path1 equals the
	set reachable by the correct fix. -/
	theorem paths_equivalent (sysGas : ℕ) :
	{s : TestState \| ∃ r g b e,
	(21000 ≤ r ∧ r ≤ sysGas) ∧ (21000 ≤ g ∧ g ≤ r) ∧ b ≤ r - g ∧
	1 ≤ e ∧ r % e = 0 ∧ s = ⟨r, e, g, b⟩} =
	{s : TestState \| ∃ r_pre g b e,
	(21000 ≤ r_pre ∧ r_pre ≤ sysGas) ∧ 1 ≤ e ∧
	21000 ≤ r_pre / e * e ∧
	(21000 ≤ g ∧ g ≤ r_pre / e * e) ∧
	b ≤ r_pre / e * e - g ∧
	s = ⟨r_pre / e * e, e, g, b⟩} := by
	ext s
	simp only [Set.mem_setOf_eq]
	constructor
	· rintro ⟨r, g, b, e, hr, hg, hb, he, hdv, rfl⟩
	obtain ⟨r_pre, hpre, he', hfl, hg', hb', heq⟩ :=
	path1_to_correct_fix hr hg hb he hdv
	exact ⟨r_pre, g, b, e, hpre, he', hfl, hg', hb', heq.symm⟩
	· rintro ⟨r_pre, g, b, e, hpre, he, hfl, hg, hb, rfl⟩
	obtain ⟨r, hr, hg', hb', he', hdv, heq⟩ :=
	correct_fix_to_path1 hpre he hfl hg hb
	exact ⟨r, g, b, e, hr, hg', hb', he', hdv, heq.symm⟩

	-- ---------------------------------------------------------------------------
	-- 6. Axiom check and sanity tests
	-- ---------------------------------------------------------------------------

	-- Confirm proof depends only on standard axioms (no sorry)
	#print axioms paths_equivalent
	#print axioms naive_fix_not_sound

	-- Concrete sanity checks (kernel-verified via decide)
	#guard (21500 / 700 * 700 : Nat) = 21000 -- rounding drops to 21000
	#guard (21000 / 255 * 255 : Nat) = 20910 -- below 21000 → vm.assume fires
	#guard (21000 / 1 * 1 : Nat) = 21000 -- e=1 always rounds cleanly
	#guard (65536 / 256 * 256 : Nat) = 65536 -- power-of-2 case

	end FuzzEquivalence

	-- =============================================================================
	-- Gas Burn Equivalence
	-- =============================================================================
	--
	-- Proves that replacing:
	-- vm.assume(_prevBaseFee * maxPercentIncrease * _gasLimit / 100 < MAX_GAS_LIMIT * 4 / 5)
	-- with a direct bound on _prevBaseFee:
	-- gasBurnDenom := maxPercentIncrease * gasLimit
	-- gasBurnCap := (MAX_GAS_LIMIT * 4/5 * 100 - 1) / gasBurnDenom (or 3 gwei if denom = 0)
	-- _prevBaseFee := bound(_prevBaseFee, 0, min(3 gwei, gasBurnCap))
	-- yields exactly the same set of reachable prevBaseFee values (modulo the
	-- acknowledged lower-bound change from 1 to 0).
	--
	-- File: packages/contracts-bedrock/test/L1/OptimismPortal2.t.sol:2664 (original)
	-- =============================================================================

	namespace GasBurnEquivalence

	/-- Core arithmetic lemma: p * m < K ↔ p ≤ (K - 1) / m, for m > 0 and K > 0.
	Forward: p * m < K → p * m ≤ K - 1 → p ≤ (K-1)/m (Euclidean floor).
	Backward: p ≤ (K-1)/m → pm ≤ (K-1)/mm ≤ K-1 < K. -/
	lemma mul_lt_iff_le_pred_div (p m K : ℕ) (hm : 0 < m) (hK : 0 < K) :
	p * m < K ↔ p ≤ (K - 1) / m := by
	constructor
	· intro h
	by_contra hlt
	push_neg at hlt
	have hmod := Nat.div_add_mod (K - 1) m
	rw [Nat.mul_comm m ((K - 1) / m)] at hmod
	-- hmod : (K - 1) / m * m + (K - 1) % m = K - 1
	have hmodlt := Nat.mod_lt (K - 1) hm
	have hmul : (K - 1) / m * m + m ≤ p * m := by
	have h1 : ((K - 1) / m + 1) * m ≤ p * m := Nat.mul_le_mul_right m hlt
	linarith [show ((K - 1) / m + 1) * m = (K - 1) / m * m + m from by ring]
	-- K - 1 uses saturating subtraction; omega handles K = (K-1) + 1 via hK
	have hK1 : K - 1 + 1 = K := by omega
	linarith
	· intro h
	have h1 := Nat.mul_le_mul_right m h
	have h2 := Nat.div_mul_le_self (K - 1) m
	omega

	/-- The gas burn condition `p * m / 100 < T` is equivalent to `p ≤ (100 * T - 1) / m`
	when m > 0 and T > 0.
	In the test: p = _prevBaseFee, m = maxPercentIncrease * _gasLimit,
	T = MAX_GAS_LIMIT * 4 / 5 = 24_000_000.
	Note: the proof's LHS set includes p = 0, whereas the original test bounded
	_prevBaseFee from 1. This is an acknowledged semantic change. -/
	lemma gas_burn_iff_bound (p m T : ℕ) (hm : 0 < m) (hT : 0 < T) :
	p * m / 100 < T ↔ p ≤ (100 * T - 1) / m := by
	-- n / 100 < T ↔ n < 100 * T (Nat.div_lt_iff_lt_mul with k = 100)
	have hdiv : p * m / 100 < T ↔ p * m < 100 * T := by omega
	rw [hdiv]
	exact mul_lt_iff_le_pred_div p m (100 * T) hm (by omega)

	/-- Main theorem: the set of prevBaseFee values satisfying the original vm.assume
	equals the set reachable by the direct bound. For m = 0 (maxPercentIncrease = 0
	or gasLimit = 0), the gas burn is always 0 < T so no cap is needed (cap = P). -/
	theorem gas_burn_paths_equivalent (P T : ℕ) (hT : 0 < T) (m : ℕ) :
	{p : ℕ \| p ≤ P ∧ p * m / 100 < T} =
	{p : ℕ \| p ≤ if m = 0 then P else min P ((100 * T - 1) / m)} := by
	ext p
	simp only [Set.mem_setOf_eq]
	by_cases hm : m = 0
	· subst hm; simp [hT]
	· have hm' : 0 < m := Nat.pos_of_ne_zero hm
	simp only [hm, ↓reduceIte, Nat.le_min, gas_burn_iff_bound p m T hm' hT]

	-- Confirm no sorry
	#print axioms gas_burn_paths_equivalent

	-- Concrete sanity checks with realistic test values (kernel-verified via decide):
	-- maxPercentIncrease = 100, gasLimit = 21000 → m = 100 * 21000 = 2_100_000
	-- T = MAX_GAS_LIMIT * 4 / 5 = 30_000_000 * 4 / 5 = 24_000_000
	-- cap = (100 * 24_000_000 - 1) / 2_100_000 = 2_399_999_999 / 2_100_000 = 1142
	#guard (100 * (30_000_000 * 4 / 5) - 1) / (100 * 21000) = 1142

	-- Verify: cap satisfies condition (cap * m / 100 < T)
	#guard (1142 * 2100000 / 100 : Nat) = 23982000 -- 23982000 < 24000000 ✓

	-- Verify: cap + 1 violates condition
	#guard (1143 * 2100000 / 100 : Nat) = 24003000 -- 24003000 ≥ 24000000 ✓

	-- Edge: m = 0 (maxPercentIncrease = 0), gas burn is always 0 < T
	#guard (999 * 0 / 100 : Nat) = 0 -- 0 < any T ✓

	end GasBurnEquivalence
No results found