Cleanup PR

.github/workflows/ci.yml

@@ -0,0 +1,79 @@
+name: CI
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+  workflow_dispatch:
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  build:
+    runs-on: ubuntu-latest
+    timeout-minutes: 330
+    steps:
+      - uses: actions/checkout@v4
+
+      # Installs the toolchain from lean-toolchain, fetches the mathlib
+      # olean cache, caches .lake in the GitHub cache, and builds the
+      # library targets.
+      - name: Build libraries
+        uses: leanprover/lean-action@v1
+        with:
+          build-args: EquiVM EVM ABI Solm Reasoning Proofs
+          use-github-cache: true
+
+      # Mirrors the imports of Examples.lean. Remove lines to prune.
+      - name: Build examples
+        run: |
+          lake build \
+            Examples.Pow.Correct \
+            Examples.Truth.Correct \
+            Examples.Caller.Correct \
+            Examples.ERC20.Correct \
+            Examples.CtorTruth.Correct \
+            Examples.CtorStore.Correct \
+            Examples.TinyImmutable.Correct \
+            Examples.Ballot.Correct \
+            Examples.SimpleAuction.Correct \
+            Examples.StringStoreLite.Correct \
+            Examples.BlindAuction.Correct \
+            Examples.OpenZeppelinBench.Ownable2Step.Correct \
+            Examples.OpenZeppelinBench.AccessControl.Correct \
+            Examples.OpenZeppelinBench.Pausable.Correct \
+            Examples.OpenZeppelinBench.ERC6909.Correct \
+            Examples.UniswapV2Pair.Correct \
+            Examples.Reuse.Correct \
+            Examples.VyperERC20.Correct
+
+      # Mirrors the imports of Benchmarks.lean. Remove lines to prune.
+      - name: Build benchmarks
+        run: |
+          lake build \
+            Benchmarks.WETH9.Correct \
+            Benchmarks.Dss.Dai.Correct \
+            Benchmarks.Dss.Jug.Correct \
+            Benchmarks.Dss.Vat.Correct \
+            Benchmarks.Dss.Pot.Correct \
+            Benchmarks.Dss.Spot.Correct \
+            Benchmarks.Dss.Vow.Correct \
+            Benchmarks.Dss.LinearDecrease.Correct \
+            Benchmarks.Dss.StairstepExponentialDecrease.Correct \
+            Benchmarks.Dss.ExponentialDecrease.Correct \
+            Benchmarks.Dss.Cat.Correct \
+            Benchmarks.Dss.Clipper.Correct \
+            Benchmarks.Dss.Cure.Correct \
+            Benchmarks.Dss.Dog.Correct \
+            Benchmarks.Dss.End.Correct \
+            Benchmarks.Dss.Flapper.Correct \
+            Benchmarks.Dss.Flipper.Correct \
+            Benchmarks.Dss.Flopper.Correct \
+            Benchmarks.Dss.GemJoin.Correct \
+            Benchmarks.Dss.DaiJoin.Correct
+
+      # Scaffolded benchmarks: specs + bytecode compile, proofs are sorry stubs.
+      - name: Build benchmark scaffolds
+        run: lake build Benchmarks.Scaffolds

ABI.lean

@@ -0,0 +1,5 @@
+import ABI.Types
+import ABI.Signature
+import ABI.Encode
+import ABI.Decode
+import ABI.StaticWords

ABI/Decode.lean

@@ -2,29 +2,32 @@ import EVM.Types
 import ABI.Types
 import Solm.Value
 
+/-! ABI decoding of calldata and return data into Solm values, parameterized by the
+compiler-specific `DecodeMode` (modern solc, legacy coder-v1 solc, Vyper). -/
+
 namespace ABI
 
 def solcMaxU64 : Nat := 18446744073709551615
 
--- Coder-v1 (solc 0.5.16 / 0.7.6) caps dynamic offsets and lengths at `2^32` *inclusive*.  Verified
--- by disassembly (`P2.h(bytes)`, `--optimize`): both the offset and length guards are
--- `PUSH5 0x0100000000; DUP; GT; ISZERO; JUMPI(→ok) else REVERT`, i.e. `GT` computes `value > 2^32`
--- and reverts iff true — so `2^32` is the largest accepted value.  (Coder v2 / `solcMaxU64` uses
--- `2^64 - 1`, and we keep applying that only in `modern`.)
+/-- Coder-v1 (solc 0.5.16 / 0.7.6) caps dynamic offsets and lengths at `2^32` *inclusive*.  Verified
+    by disassembly (`P2.h(bytes)`, `--optimize`): both the offset and length guards are
+    `PUSH5 0x0100000000; DUP; GT; ISZERO; JUMPI(→ok) else REVERT`, i.e. `GT` computes `value > 2^32`
+    and reverts iff true — so `2^32` is the largest accepted value.  (Coder v2 / `solcMaxU64` uses
+    `2^64 - 1`, and we keep applying that only in `modern`.) -/
 def solcMaxLenV1 : Nat := 4294967296  -- 2^32
 
 def solcMaxLen : DecodeMode → Nat
   | DecodeMode.modern       => solcMaxU64
   | DecodeMode.vyper        => solcMaxU64
   | DecodeMode.legacySolc05 => solcMaxLenV1
 
--- In `modern` the dynamic cap is exactly `solcMaxU64`, so `modern`-mode decode proofs that unfold the
--- guards reduce back to the pre-existing `solcMaxU64 < …` shape (statements unchanged).
+/-- In `modern` the dynamic cap is exactly `solcMaxU64`, so `modern`-mode decode proofs that unfold
+    the guards reduce back to the pre-existing `solcMaxU64 < …` shape (statements unchanged). -/
 @[simp] theorem solcMaxLen_modern : solcMaxLen DecodeMode.modern = solcMaxU64 := rfl
 
--- Modern solc nested dynamic-array decoders do not reject an element's relative offset just because
--- it is larger than `2^64 - 1`; the generated bytecode relies on signed calldata-bounds checks for
--- the target. Legacy coder-v1 keeps the old inclusive `2^32` offset cap.
+/-- Modern solc nested dynamic-array decoders do not reject an element's relative offset just because
+    it is larger than `2^64 - 1`; the generated bytecode relies on signed calldata-bounds checks for
+    the target. Legacy coder-v1 keeps the old inclusive `2^32` offset cap. -/
 def solcRejectsDynamicArrayElementOffset (mode : DecodeMode) (relativeOffset : Nat) : Bool :=
   match mode with
   | DecodeMode.modern => false
@@ -476,9 +479,9 @@ def decodeReturnValuesWithMode? (mode : DecodeMode) (types : List ABIType) (retu
         decodeABIValues? types bytes 0 0 headSize headSize DecodeMode.legacySolc05
       some values
 
--- Decodes a single top-level value.  For a callee's multi-value return use `decodeReturnValues?` —
--- a `.tuple` type here is one tuple-typed output (ABI-wrapped, with a leading offset word), NOT a
--- flat multi-return.
+/-- Decodes a single top-level value.  For a callee's multi-value return use `decodeReturnValues?` —
+    a `.tuple` type here is one tuple-typed output (ABI-wrapped, with a leading offset word), NOT a
+    flat multi-return. -/
 def decodeReturnValue? (ty : ABIType) (returndata : ByteArray) : Option Solm.Value := do
   match decodeReturnValues? [ty] returndata with
   | some [value] => some value

ABI/Encode.lean

@@ -2,6 +2,8 @@ import EVM.Types
 import ABI.Types
 import Solm.Value
 
+/-! ABI encoding of Solm values -/
+
 namespace ABI
 
 def natBytes (n : Nat) : List UInt8 :=

ABI/Signature.lean

@@ -1,5 +1,7 @@
 import ABI.Types
 
+/-! Function signatures and their canonical string form, as hashed for the 4-byte selector. -/
+
 namespace ABI
 
 structure Signature where

ABI/StaticWords.lean

@@ -1,6 +1,8 @@
 import ABI.Encode
 import ABI.Decode
 
+/-! Flattening static ABI types into the word-scalar leaves they occupy. -/
+
 namespace ABI
 
 /-- Repeat a list `n` times and concatenate the copies. -/
@@ -41,8 +43,7 @@ end
 mutual
   /-- Flatten a static ABI value into `(type, value)` word-scalar leaves, in ABI order.
 
-  The function succeeds only when every scalar leaf is accepted by `encodeABIWord?`; this makes it
-  a convenient domain predicate for word-level encoder theorems.
+  The function succeeds only when every scalar leaf is accepted by `encodeABIWord?`.
   -/
   def staticWordPairs? : ABIType → Solm.Value → Option (List (ABIType × Solm.Value))
     | ty@(.elem _), value =>

ABI/Types.lean

@@ -1,3 +1,4 @@
+/-! The Solidity ABI type grammar, and static size/dynamicity computations over it. -/
 
 namespace ABI
 
@@ -7,20 +8,20 @@ def BitWidth := { m : Nat // 0 < m ∧ m ≤ 256 ∧ m % 8 = 0}
 def FinPos N := { n : Nat // 0 < n ∧ n ≤ N }
   deriving DecidableEq, Repr
 
-/- Integer types used by Solidity-style ABI values. -/
+/-- Integer types used by Solidity-style ABI values. -/
 inductive IntType where
   | uint : BitWidth -> IntType
   | sint : BitWidth -> IntType
   deriving DecidableEq, Repr
 
-/- Fixed-point decimal number types used by Solidity-style ABI values. -/
+/-- Fixed-point decimal number types used by Solidity-style ABI values. -/
 -- Note: Just added to have complete coverage of ABI, will not implement right now
 inductive FixedType where
   | ufixed : BitWidth -> FinPos 80 -> FixedType
   | fixed : BitWidth -> FinPos 81 -> FixedType
   deriving DecidableEq, Repr
 
-/- Elemnrary first-order types, per the Solidity ABI. -/
+/-- Elementary first-order types, per the Solidity ABI. -/
 inductive ElemType where
   | bool : ElemType
   | address : ElemType
@@ -30,19 +31,19 @@ inductive ElemType where
   | function : ElemType
   deriving DecidableEq, Repr, Inhabited
 
-/- ABI decoder mode for compiler-specific wrapper behavior. Modern solc decoders reject
-   non-canonical value words and use signed size guards. Legacy solc (coder v1) instead *cleans*
-   value types rather than validating them: normalize `bool` (nonzero → true), mask `address`, and
-   mask narrow `uintN` — using unsigned static-size checks. . Vyper fixed-argument wrappers keep
-   canonical address checks but use minimum static-size checks rather than solc's signed
-   huge-calldata guard. -/
+/-- ABI decoder mode for compiler-specific wrapper behavior. Modern solc decoders reject
+    non-canonical value words and use signed size guards. Legacy solc (coder v1) instead *cleans*
+    value types rather than validating them: normalize `bool` (nonzero → true), mask `address`, and
+    mask narrow `uintN` — using unsigned static-size checks. Vyper fixed-argument wrappers keep
+    canonical address checks but use minimum static-size checks rather than solc's signed
+    huge-calldata guard. -/
 inductive DecodeMode where
   | modern : DecodeMode
   | legacySolc05 : DecodeMode
   | vyper : DecodeMode
   deriving DecidableEq, Repr, Inhabited
 
-/- ABI types for parameters, locals, and return values. -/
+/-- ABI types for parameters, locals, and return values. -/
 inductive ABIType where
   | elem : ElemType -> ABIType
   | array : ABIType -> Nat -> ABIType
@@ -132,8 +133,6 @@ mutual
     | ty :: tys => isDynamicABIType ty || isDynamicABITypeList tys
 end
 
-def usesLegacyAddressTypes (_types : List ABIType) : Bool := false
-
 mutual
   def staticABIEncodedSize? : ABIType → Option Nat
     | .elem _ => some 32

Benchmarks.lean

@@ -1,7 +1,4 @@
 import Benchmarks.WETH9.Correct
-import Benchmarks.Safe.Correct
-import Benchmarks.UniswapV3Pool.Correct
-import Benchmarks.UniswapV2Router02.Correct
 import Benchmarks.Dss.Dai.Correct
 import Benchmarks.Dss.Jug.Correct
 import Benchmarks.Dss.Vat.Correct
@@ -21,11 +18,3 @@ import Benchmarks.Dss.Flipper.Correct
 import Benchmarks.Dss.Flopper.Correct
 import Benchmarks.Dss.GemJoin.Correct
 import Benchmarks.Dss.DaiJoin.Correct
-import Benchmarks.CompoundIII.CometRewards.Correct
-import Benchmarks.CompoundIII.Comet.Correct
-import Benchmarks.EAS.Attester.Correct
-import Benchmarks.ERC721.Correct
-import Benchmarks.Auction.Correct
-import Benchmarks.OpenZeppelinBench.VestingWallet.Correct
-import Benchmarks.OpenZeppelinBench.TimelockController.Correct
-import Benchmarks.Klima.Correct