feat(EVM,Trace,Core): land ERC-4337 frame primitives upstream

AXIOMS.md

@@ -185,6 +185,29 @@ to contracts that use the module. The compiler lists all of them at compile
 time in `--verbose` output. Use `--deny-unchecked-dependencies` to make
 compilation fail if any assumption hasn't been reviewed.
 
+### Caller-frame preservation theorems
+
+Independently of the ECM interface assumptions above, the *EVM frame
+condition* that an external `CALL` cannot mutate the caller's storage,
+transient storage, or memory outside the declared output buffer is now a
+**theorem** of `Verity.EVM.Frame`, no longer an assumption. The relevant
+results are:
+
+- `Verity.EVM.Frame.external_call_preserves_caller_storage`
+- `Verity.EVM.Frame.external_call_preserves_caller_transient_storage`
+- `Verity.EVM.Frame.external_call_preserves_caller_memory_outside_output_buffer`
+- `Verity.EVM.Frame.external_call_preserves_caller_memory` (disjoint-region form)
+- their iterated-CALL variants `Verity.EVM.Frame.external_calls_preserve_*`
+
+The theorems quantify universally over `Verity.EVM.Frame.CalleeResult`,
+which is the observational interface of any EVM callee program. Downstream
+contract proofs can consume these theorems directly to discharge the EVM
+frame condition without re-stating it.
+
+The abstract memory model on which these theorems compose lives at
+`Verity.EVM.MemoryModel`; the standard solc memory-layout schema and the
+call-buffer-disjoint-from-heap theorem live at `Verity.EVM.Layout`.
+
 ### Standard Module Assumptions
 
 | Module | Assumption | Meaning |

Contracts/Common.lean

@@ -13,6 +13,14 @@ open Verity.EVM.Uint256
 open Verity.Stdlib.Math
 
 macro_rules
+  -- DSL ergonomics: rewrite `let _ := rhs` into a do-block-friendly form
+  -- so that consumers can discard an external-call result naturally.
+  -- (Without this rule the verity_contract function-body parser rejects
+  -- `let _ := …` as an unsupported do element.)
+  | `(doElem| let _ := $rhs:term) => do
+      let fresh ← Lean.Macro.addMacroScope `_callResult
+      let freshIdent := Lean.mkIdent fresh
+      `(doElem| let $freshIdent := $rhs)
   | `(term| ecmCall $_moduleFactory:term $_args:term) =>
       `(term| do
           let _ := $_moduleFactory

TRUST_ASSUMPTIONS.md

@@ -78,6 +78,7 @@ Current theorem totals, property-test coverage, and proof status live in [docs/V
 - **Role**: Reusable typed external call patterns (ERC-20 writes/reads including `totalSupply`, ERC-4626 preview/conversion helpers plus `totalAssets`, `asset`, `max*` limit reads, and `deposit`, oracle reads, precompiles 0x01 / 0x02 / 0x06 / 0x07 / 0x08 — `ecrecover`, `sha256`, BN254 `bn256Add`, `bn256ScalarMul`, `bn256Pairing` — callbacks).
 - **Trust**: Each module's `compile` produces correct Yul. Bug in one module doesn't affect others.
 - **Mitigation**: Axiom aggregation at compile time (`--verbose`), machine-readable trust-surface emission via `--trust-report <path>`, and a fail-closed verification gate via `--deny-unchecked-dependencies` when unchecked foreign surfaces must be excluded. See [docs/EXTERNAL_CALL_MODULES.md](docs/EXTERNAL_CALL_MODULES.md).
+- **Caller-frame preservation**: The EVM frame condition (external `CALL` cannot mutate caller storage / transient storage / memory outside the declared output buffer) is now a *theorem* of `Verity.EVM.Frame` rather than an assumption. Downstream proofs consume `external_call_preserves_caller_storage` etc. directly. The abstract memory model used by these theorems is `Verity.EVM.MemoryModel`; the solc memory-layout schema and call-buffer-disjoint-from-heap result are in `Verity.EVM.Layout`. EvmYul ↔ abstract-model correspondence remains the open follow-up.
 
 ### 8. Lean Kernel
 - **Role**: Proof checker soundness. Foundational assumption for all Lean-based verification.

Verity/Compiler/FromSolidity.lean

@@ -0,0 +1,142 @@
+import Lean
+
+namespace Verity.Compiler.FromSolidity
+
+open Lean Elab Command
+
+/-!
+# `#fromSolidity` Lean entry point — scaffold
+
+Today the Verity compiler runs out-of-band via the `verity-cli`
+command-line tool: a developer manually invokes
+`verity-cli compile path/to/Foo.sol --emit lean` and copies the
+generated Lean term into the benchmark.
+
+This module is the **scaffold** for surfacing that pipeline as a Lean
+elaborator-level command, so that a benchmark file can declare:
+
+```
+#fromSolidity "vendor/account-abstraction/EntryPoint.sol"
+```
+
+and obtain a proof-checked `verity_contract` term as if it had been
+hand-written.
+
+## Status
+
+This scaffold lands the public API surface (`#fromSolidity` command,
+options, error type) and a stub elaborator that defers to the CLI via
+`IO.Process.run`. The full machine translation requires hooking
+`Compiler/CompilationModel.lean`'s Solidity-IR pipeline directly into
+Lean's elaborator, which is a multi-week project tracked separately
+(see `docs/ROADMAP.md` "machine fromSolidity").
+
+The scaffold exists so:
+
+* The API contract is fixed (the command name and option shape will not
+  change underneath downstream benchmarks).
+* The CLI integration point is documented as a single function
+  (`runVerityCliCompile`) that the next PR replaces with an in-process
+  call.
+* Benchmarks that today write `verity_contract` blocks by hand can
+  switch to `#fromSolidity` once the CLI shells out cleanly, without
+  changing their proof files.
+
+## Trust boundary today vs. after full implementation
+
+Today (`fromSolidity` shells out to `verity-cli`):
+* Trust the CLI binary on disk.
+* Trust the file-system path is consistent with what the developer
+  proved against.
+
+After full implementation (in-process):
+* No CLI binary trust — translation runs inside Lean.
+* The same kernel checks the resulting term that checks every Lean
+  proof.
+
+The headline difference: the post-implementation form makes
+*translation faithfulness* part of the proof-checked trust base.
+-/
+
+/-- Options for `#fromSolidity`. -/
+structure Options where
+  /-- Path to the Solidity source. Resolved relative to the workspace root. -/
+  path : System.FilePath
+  /-- Optional contract name selector (defaults to the only contract in the file). -/
+  contractName : Option String := none
+  /-- Verity CLI binary to invoke. Defaults to `verity-cli` on PATH. -/
+  cliBinary : String := "verity-cli"
+  deriving Repr
+
+/-- Result of running the CLI translation step. -/
+inductive Result where
+  | ok (lean : String)
+  | error (msg : String)
+  deriving Repr
+
+/-- Locate the Lake workspace root containing the current process, if any. -/
+partial def findWorkspaceRoot? (dir : System.FilePath) : IO (Option System.FilePath) := do
+  if ← (dir / "lakefile.lean").pathExists then
+    pure (some dir)
+  else if ← (dir / "lakefile.toml").pathExists then
+    pure (some dir)
+  else
+    match dir.parent with
+    | some parent =>
+        if parent == dir then
+          pure none
+        else
+          findWorkspaceRoot? parent
+    | none => pure none
+
+/-- Resolve `path` according to the `Options.path` contract.
+
+Absolute paths are preserved. Relative paths are anchored at the Lake workspace
+root containing the current process, falling back to the process working
+directory when the command is run outside a Lake workspace. -/
+def resolveSourcePath (path : System.FilePath) : IO System.FilePath := do
+  if path.isAbsolute then
+    pure path.normalize
+  else
+    let cwd ← IO.currentDir
+    let root ← findWorkspaceRoot? cwd
+    pure (((root.getD cwd) / path).normalize)
+
+/-- Invoke `verity-cli compile path --emit lean`. Returns the emitted
+    Lean source on stdout or an error message. -/
+def runVerityCliCompile (opts : Options) : IO Result := do
+  let sourcePath ← resolveSourcePath opts.path
+  let args := match opts.contractName with
+    | some c =>
+        #["compile", sourcePath.toString, "--contract", c, "--emit", "lean"]
+    | none =>
+        #["compile", sourcePath.toString, "--emit", "lean"]
+  try
+    let out ← IO.Process.run { cmd := opts.cliBinary, args }
+    return .ok out
+  catch e =>
+    return .error s!"verity-cli failed: {e.toString}"
+
+/-- `#fromSolidity "path"` command. Currently emits a placeholder
+    `axiom` whose name documents the pending translation; replace with a
+    proper elaborator emission once the in-process translator lands. -/
+syntax (name := fromSolidityCmd) "#fromSolidity " str (" contract " str)? : command
+
+@[command_elab fromSolidityCmd]
+def elabFromSolidity : CommandElab := fun stx => do
+  let pathLit := stx[1]
+  let path : System.FilePath := pathLit.isStrLit?.get!
+  let contractOpt : Option String :=
+    if stx[2].getNumArgs > 0 then some stx[2][1].isStrLit?.get! else none
+  let opts : Options := { path := path, contractName := contractOpt }
+  let result : Result ← (runVerityCliCompile opts).toIO
+    (fun e => IO.userError s!"fromSolidity IO failure: {e.toString}")
+  match result with
+  | .ok _emitted =>
+      let sourcePath ← (resolveSourcePath opts.path).toIO
+        (fun e => IO.userError s!"fromSolidity path resolution failure: {e.toString}")
+      logInfo m!"fromSolidity scaffold: would elaborate {sourcePath}; in-process translator pending"
+  | .error msg =>
+      throwError m!"fromSolidity: {msg}. Falling back: declare the verity_contract block by hand for now."
+
+end Verity.Compiler.FromSolidity

Verity/Core.lean

@@ -621,6 +621,52 @@ theorem require_succeeds (cond : Bool) (msg : String) (s : ContractState) :
     simp [hLocked]
   simp [Contract.run, nonReentrant, hNe]
 
+/-- EIP-1153 transient-storage reentrancy guard primitive.
+
+Uses the transient-storage slot at `lockOffset` as a mutex (`0` = unlocked,
+nonzero = locked), sets it before running `body`, and clears it on both
+success and revert paths. Mirrors OpenZeppelin's `ReentrancyGuardTransient`.
+
+The transient-storage variant is preferred over storage-slot
+`nonReentrant` for new contracts: it is automatically cleared at the end
+of every transaction, eliminating the upgrade-related storage-layout
+concerns of storage-slot guards. -/
+def nonReentrantTransient (lockOffset : Uint256) (body : Contract α) : Contract α :=
+  fun s =>
+    if s.transientStorage (lockOffset : Nat) == 0 then
+      let sLocked := { s with
+        transientStorage := fun i =>
+          if i == (lockOffset : Nat) then 1 else s.transientStorage i }
+      match body sLocked with
+      | ContractResult.success a s' =>
+          ContractResult.success a
+            { s' with
+              transientStorage := fun i =>
+                if i == (lockOffset : Nat) then 0 else s'.transientStorage i }
+      | ContractResult.revert msg s' =>
+          ContractResult.revert msg
+            { s' with
+              transientStorage := fun i =>
+                if i == (lockOffset : Nat) then 0 else s'.transientStorage i }
+    else
+      ContractResult.revert "ReentrancyGuardTransient: reentrant call" s
+
+@[simp] theorem nonReentrantTransient_locked_reverts
+    (lockOffset : Uint256) (body : Contract α) (s : ContractState)
+    (hLocked : s.transientStorage (lockOffset : Nat) ≠ 0) :
+    (nonReentrantTransient lockOffset body).run s =
+      ContractResult.revert "ReentrancyGuardTransient: reentrant call" s := by
+  have hNe : (s.transientStorage (lockOffset : Nat) == 0) = false := by
+    simp [hLocked]
+  simp [Contract.run, nonReentrantTransient, hNe]
+
+theorem nonReentrantTransient_revert_preserves_state
+    (lockOffset : Uint256) (body : Contract α) (s : ContractState)
+    (hLocked : s.transientStorage (lockOffset : Nat) ≠ 0) :
+    ((nonReentrantTransient lockOffset body).run s).snd = s := by
+  rw [nonReentrantTransient_locked_reverts lockOffset body s hLocked]
+  rfl
+
 -- Regression for #254: mutations before a revert do not leak through `run`.
 theorem run_revert_rolls_back_storage (value : Uint256) (s : ContractState) :
   ((bind (setStorage ⟨0⟩ value) (fun _ => require false "revert")).run s) =