Add formally verified natural logarithm

.github/workflows/ln-formal.yml

@@ -0,0 +1,125 @@
+name: Ln.sol Formal Check
+
+on:
+  push:
+    branches:
+      - master
+    paths:
+      - src/vendor/Ln.sol
+      - src/wrappers/LnWrapper.sol
+      - formal/ln/**
+      - formal/python/**
+      - test/0.8.34/Ln.t.sol
+      - test/0.8.25/formal-model/FormalModelFFI.t.sol
+      - test/0.8.25/formal-model/LnModel.t.sol
+      - .github/workflows/ln-formal.yml
+  pull_request:
+    paths:
+      - src/vendor/Ln.sol
+      - src/wrappers/LnWrapper.sol
+      - formal/ln/**
+      - formal/python/**
+      - test/0.8.34/Ln.t.sol
+      - test/0.8.25/formal-model/FormalModelFFI.t.sol
+      - test/0.8.25/formal-model/LnModel.t.sol
+      - .github/workflows/ln-formal.yml
+
+jobs:
+  ln-formal:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Install Foundry
+        uses: foundry-rs/foundry-toolchain@v1
+
+      - name: Install Python
+        uses: actions/setup-python@v5
+        with:
+          python-version: "3.11"
+
+      - name: Install pinned Lean toolchain
+        run: |
+          curl https://raw.githubusercontent.com/leanprover/elan/917c18d0ad52f649c2603dc8b973f5b9fa5f8f43/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+          LEAN_TOOLCHAIN="$(cat formal/ln/LnProof/lean-toolchain)"
+          "$HOME/.elan/bin/elan" toolchain install "$LEAN_TOOLCHAIN"
+          "$HOME/.elan/bin/elan" default "$LEAN_TOOLCHAIN"
+
+      - name: Install solc 0.8.34
+        run: forge build -- src/chains/Mainnet/TakerSubmitted.sol
+        env:
+          FOUNDRY_SOLC_VERSION: 0.8.34
+
+      - name: Check floor-specification witness and helper mirror
+        run: python3 -W error -m formal.python.ln.check_ln_counterexample
+
+      - name: Check monotonicity certificate
+        run: python3 -W error -m formal.python.ln.check_ln_monotone
+
+      - name: Generate Lean model from Ln.sol via Yul IR
+        run: |
+          forge inspect src/wrappers/LnWrapper.sol:LnWrapper ir | \
+            python3 -W error -m formal.python.ln.generate_ln_model \
+              --yul - \
+              --output formal/ln/LnProof/LnProof/GeneratedLnModel.lean
+
+      - name: Generate certificate coefficient literals
+        run: python3 -W error formal/python/ln/gen_cert_literals.py
+
+      - name: Build Ln proof and model evaluator
+        working-directory: formal/ln/LnProof
+        run: lake build && lake build ln-model
+
+      - name: Check proof axioms
+        working-directory: formal/ln/LnProof
+        run: |
+          printf '%s\n' \
+            'import LnProof.TopMono' \
+            'import LnProof.FloorSpec' \
+            'import LnProof.ExpLogCutSpec' \
+            '#print axioms LnGeneratedModel.model_ln_wad_one_wad' \
+            '#print axioms LnGeneratedModel.model_ln_wad_to_wad_one_wad' \
+            '#print axioms LnGeneratedModel.model_ln_wad_one_wad_mono' \
+            '#print axioms LnGeneratedModel.model_ln_wad_seam_mono' \
+            '#print axioms LnGeneratedModel.model_ln_wad_to_wad_seam_mono' \
+            '#print axioms LnGeneratedModel.model_ln_wad_mono' \
+            '#print axioms LnGeneratedModel.model_ln_wad_to_wad_mono' \
+            '#print axioms LnFloorCert.model_ln_wad_floor' \
+            '#print axioms LnFloorCert.model_ln_wad_to_wad_floor' \
+            '#print axioms LnFloorCert.model_ln_wad_negative_iff' \
+            '#print axioms LnFloorCert.model_ln_wad_to_wad_negative_iff' \
+            '#print axioms LnFloorCert.FloorSpecA_iff_cutLeLogWadRay' \
+            '#print axioms LnFloorCert.FloorSpecB_iff_cutLogWadRayLtWithMargin' \
+            '#print axioms LnFloorCert.FloorSpec_iff_cutLnWadRayBracket' \
+            '#print axioms LnFloorCert.FloorSpecToWad_iff_cutLnWadSpec' \
+            '#print axioms LnFloorCert.model_ln_wad_cut_spec' \
+            '#print axioms LnFloorCert.model_ln_wad_to_wad_cut_spec' \
+            | lake env lean --stdin > actual_axioms.txt 2>&1
+          diff -u --label expected --label actual - actual_axioms.txt <<'EXPECTED'
+          'LnGeneratedModel.model_ln_wad_one_wad' does not depend on any axioms
+          'LnGeneratedModel.model_ln_wad_to_wad_one_wad' does not depend on any axioms
+          'LnGeneratedModel.model_ln_wad_one_wad_mono' does not depend on any axioms
+          'LnGeneratedModel.model_ln_wad_seam_mono' does not depend on any axioms
+          'LnGeneratedModel.model_ln_wad_to_wad_seam_mono' does not depend on any axioms
+          'LnGeneratedModel.model_ln_wad_mono' depends on axioms: [propext, Classical.choice, Quot.sound]
+          'LnGeneratedModel.model_ln_wad_to_wad_mono' depends on axioms: [propext, Classical.choice, Quot.sound]
+          'LnFloorCert.model_ln_wad_floor' depends on axioms: [propext, Classical.choice, Quot.sound]
+          'LnFloorCert.model_ln_wad_to_wad_floor' depends on axioms: [propext, Classical.choice, Quot.sound]
+          'LnFloorCert.model_ln_wad_negative_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
+          'LnFloorCert.model_ln_wad_to_wad_negative_iff' depends on axioms: [propext, Classical.choice, Quot.sound]
+          'LnFloorCert.FloorSpecA_iff_cutLeLogWadRay' depends on axioms: [propext]
+          'LnFloorCert.FloorSpecB_iff_cutLogWadRayLtWithMargin' depends on axioms: [propext, Quot.sound]
+          'LnFloorCert.FloorSpec_iff_cutLnWadRayBracket' depends on axioms: [propext, Quot.sound]
+          'LnFloorCert.FloorSpecToWad_iff_cutLnWadSpec' depends on axioms: [propext, Quot.sound]
+          'LnFloorCert.model_ln_wad_cut_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
+          'LnFloorCert.model_ln_wad_to_wad_cut_spec' depends on axioms: [propext, Classical.choice, Quot.sound]
+          EXPECTED
+
+      - name: Fuzz-test Lean model against Solidity
+        run: |
+          FOUNDRY_PROFILE=formal-model forge test \
+            --skip 'src/*' --skip 'test/unit/*' --skip 'test/integration/*' --skip 'test/0.8.28/*' \
+            --match-contract LnModelTest

formal/ln/LnProof/.gitignore

@@ -0,0 +1,12 @@
+/.lake/
+/actual_axioms.txt
+
+# Auto-generated; rebuild with:
+#   forge inspect src/wrappers/LnWrapper.sol:LnWrapper ir | \
+#     python3 -m formal.python.ln.generate_ln_model --yul - \
+#       --output formal/ln/LnProof/LnProof/GeneratedLnModel.lean
+/LnProof/GeneratedLnModel.lean
+
+# Auto-generated; rebuild with:
+#   python3 formal/python/ln/gen_cert_literals.py
+/LnProof/FloorCertLit.lean

formal/ln/LnProof/LnProof.lean

@@ -0,0 +1,7 @@
+-- This module serves as the root of the `LnProof` library.
+-- Import modules here that should be built as part of the library.
+import LnProof.GeneratedLnModel
+import LnProof.LnMono
+import LnProof.TopMono
+import LnProof.FloorSpec
+import LnProof.ExpLogCutSpec

formal/ln/LnProof/LnProof/Bridge.lean

@@ -0,0 +1,136 @@
+import LnProof.GeneratedLnModel
+
+/-!
+# Two's-complement transport lemmas
+
+`toInt` is the signed view of a uint256 word; each lemma here transports one
+modeled EVM opcode to plain `Int` arithmetic under explicit range hypotheses
+(no overflow, divisor nonzero, ...). Everything downstream reasons in `Int`.
+-/
+
+namespace LnGeneratedModel
+
+def toInt (w : Nat) : Int :=
+  if w < 2 ^ 255 then (w : Int) else (w : Int) - 2 ^ 256
+
+def ofInt (x : Int) : Nat := (x % (2 ^ 256 : Int)).toNat
+
+/-- `omega` needs numeral divisors for `Int.emod`; these rewrite the powers. -/
+theorem ipow256 :
+    (2 : Int) ^ 256 =
+      115792089237316195423570985008687907853269984665640564039457584007913129639936 := by
+  rfl
+
+theorem ipow255 :
+    (2 : Int) ^ 255 =
+      57896044618658097711785492504343953926634992332820282019728792003956564819968 := by
+  rfl
+
+theorem word_mod_eq : WORD_MOD = 2 ^ 256 := rfl
+
+theorem u256_eq (w : Nat) : u256 w = w % 2 ^ 256 := rfl
+
+theorem u256_of_lt {w : Nat} (h : w < 2 ^ 256) : u256 w = w := by
+  simp [u256_eq, Nat.mod_eq_of_lt h]
+
+theorem toInt_lt {w : Nat} (h : w < 2 ^ 256) : toInt w < 2 ^ 255 := by
+  unfold toInt; simp only [ipow255, ipow256]; split <;> omega
+
+theorem toInt_ge {w : Nat} (h : w < 2 ^ 256) : -(2 ^ 255) ≤ toInt w := by
+  unfold toInt; simp only [ipow255, ipow256]; split <;> omega
+
+theorem toInt_of_lt {w : Nat} (h : w < 2 ^ 255) : toInt w = (w : Int) := by
+  unfold toInt; split <;> omega
+
+theorem ofInt_lt (x : Int) : ofInt x < 2 ^ 256 := by
+  unfold ofInt; simp only [ipow256]; omega
+
+theorem toInt_ofInt {x : Int} (h1 : -(2 ^ 255) ≤ x) (h2 : x < 2 ^ 255) :
+    toInt (ofInt x) = x := by
+  unfold toInt ofInt
+  simp only [ipow255, ipow256] at *
+  split <;> omega
+
+theorem ofInt_toInt {w : Nat} (h : w < 2 ^ 256) : ofInt (toInt w) = w := by
+  unfold toInt ofInt
+  simp only [ipow256] at *
+  split <;> omega
+
+/-- `sle` (the comparison used by the seam theorems) agrees with `Int`
+ordering of the signed views. -/
+def sleInt (a b : Nat) : Bool :=
+  decide ((a + 2 ^ 255) % WORD_MOD ≤ (b + 2 ^ 255) % WORD_MOD)
+
+theorem sleInt_iff {a b : Nat} (ha : a < 2 ^ 256) (hb : b < 2 ^ 256) :
+    sleInt a b = true ↔ toInt a ≤ toInt b := by
+  unfold sleInt toInt
+  simp only [word_mod_eq, decide_eq_true_eq, ipow256]
+  split <;> split <;> omega
+
+/-! ## Opcode transports -/
+
+/-- Master wrap lemma: a Nat congruent to `x` mod `2^256` decodes to `x` when
+`x` is in signed range. -/
+theorem toInt_wrap {n : Nat} {x : Int}
+    (key : (n : Int) % (2 ^ 256 : Int) = x % (2 ^ 256 : Int))
+    (h1 : -(2 ^ 255) ≤ x) (h2 : x < 2 ^ 255) :
+    toInt (n % 2 ^ 256) = x := by
+  unfold toInt
+  simp only [ipow255, ipow256] at *
+  split <;> omega
+
+theorem toInt_mod_cong {w : Nat} (_h : w < 2 ^ 256) :
+    (w : Int) % (2 ^ 256 : Int) = toInt w % (2 ^ 256 : Int) := by
+  unfold toInt
+  simp only [ipow256] at *
+  split <;> omega
+
+theorem evmAdd_eq (a b : Nat) : evmAdd a b = (a + b) % 2 ^ 256 := by
+  unfold evmAdd u256; simp only [word_mod_eq]; omega
+
+theorem evmSub_eq {a b : Nat} (ha : a < 2 ^ 256) (hb : b < 2 ^ 256) :
+    evmSub a b = (a + 2 ^ 256 - b) % 2 ^ 256 := by
+  unfold evmSub u256; simp only [word_mod_eq]
+  rw [Nat.mod_eq_of_lt ha, Nat.mod_eq_of_lt hb]
+
+theorem evmMul_eq {a b : Nat} (ha : a < 2 ^ 256) (hb : b < 2 ^ 256) :
+    evmMul a b = (a * b) % 2 ^ 256 := by
+  unfold evmMul u256; simp only [word_mod_eq]
+  rw [Nat.mod_eq_of_lt ha, Nat.mod_eq_of_lt hb]
+
+theorem evmAdd_lt (a b : Nat) : evmAdd a b < 2 ^ 256 := by
+  unfold evmAdd u256; simp only [word_mod_eq]; omega
+
+theorem evmSub_lt (a b : Nat) : evmSub a b < 2 ^ 256 := by
+  unfold evmSub u256; simp only [word_mod_eq]; omega
+
+theorem evmMul_lt (a b : Nat) : evmMul a b < 2 ^ 256 := by
+  unfold evmMul u256; simp only [word_mod_eq]; omega
+
+theorem evmAdd_transport {a b : Nat} (ha : a < 2 ^ 256) (hb : b < 2 ^ 256)
+    (h1 : -(2 ^ 255) ≤ toInt a + toInt b) (h2 : toInt a + toInt b < 2 ^ 255) :
+    toInt (evmAdd a b) = toInt a + toInt b := by
+  rw [evmAdd_eq a b]
+  refine toInt_wrap ?_ h1 h2
+  have hc : ((a + b : Nat) : Int) = (a : Int) + (b : Int) := by omega
+  rw [hc, Int.add_emod, toInt_mod_cong ha, toInt_mod_cong hb, ← Int.add_emod]
+
+theorem evmSub_transport {a b : Nat} (ha : a < 2 ^ 256) (hb : b < 2 ^ 256)
+    (h1 : -(2 ^ 255) ≤ toInt a - toInt b) (h2 : toInt a - toInt b < 2 ^ 255) :
+    toInt (evmSub a b) = toInt a - toInt b := by
+  rw [evmSub_eq ha hb]
+  refine toInt_wrap ?_ h1 h2
+  have hc : ((a + 2 ^ 256 - b : Nat) : Int) = (a : Int) - (b : Int) + 2 ^ 256 := by
+    simp only [ipow256]; omega
+  rw [hc, Int.add_emod_right, Int.sub_emod, toInt_mod_cong ha, toInt_mod_cong hb,
+    ← Int.sub_emod]
+
+theorem evmMul_transport {a b : Nat} (ha : a < 2 ^ 256) (hb : b < 2 ^ 256)
+    (h1 : -(2 ^ 255) ≤ toInt a * toInt b) (h2 : toInt a * toInt b < 2 ^ 255) :
+    toInt (evmMul a b) = toInt a * toInt b := by
+  rw [evmMul_eq ha hb]
+  refine toInt_wrap ?_ h1 h2
+  have hc : ((a * b : Nat) : Int) = (a : Int) * (b : Int) := by exact_mod_cast rfl
+  rw [hc, Int.mul_emod, toInt_mod_cong ha, toInt_mod_cong hb, ← Int.mul_emod]
+
+end LnGeneratedModel