Prove Step is not deterministic (Aristotle counterexample)

[leonardoalt]

Summary

Settles the question "is the small-step relation Step deterministic?" — it is not, and this PR adds a machine-checked disproof produced by @Aristotle-Harmonic (project 215f4cdc-5cec-4ef5-8d40-2772b46e90ac).

New module EvmSemantics/EVM/StepDeterminism.lean:

• underdeterminedState — a fully concrete witness: the default State with its bytecode overridden to the single byte 0x01 (ADD). All other fields keep their defaults: halt = .Running, stack = [], gasAvailable = 0, and the zero codeAddr (not a precompile).
• theorem step_not_deterministic : ∃ (s s₁ s₂ : State), Step s s₁ ∧ Step s s₂ ∧ s₁ ≠ s₂ — sorry-free, axiom footprint [propext, Classical.choice, Quot.sound] (pinned by a trailing #print axioms).

Why it's non-deterministic

Exactly the overlap the comment at the top of StepRunning's exception-rules section already anticipated: the exception rules' premises are not mutually exclusive. On the witness state both

• StepRunning.stackUnderflow fires (ADD has popArity = 2, stack length 0), yielding halt := .Exception .StackUnderflow, and
• StepRunning.outOfGas fires (cost witness 1, gasAvailable = 0 < 1 ≤ Gas.totalCost), yielding halt := .Exception .OutOfGas.

Both lift through Step.running (the s.halt = .Running and isPrecompile … = false gates hold), and the successors differ in halt — two distinct post-states from one pre-state.

This is non-determinism only in which exception is reported; a deterministic check order (as stepF implements) can be layered on top, which is what stepF_sound already witnesses one direction of.

Commits

• aristotle: prove Step is not deterministic … — Aristotle's output, as-is.
• Remove Aristotle attribution boilerplate — drops the README ad header and ARISTOTLE_SUMMARY.md it also added.

Verification

• lake build evm_semantics vmtests from a clean .lake/build: success (1089 jobs), zero warning: lines.
• lake lint: passed.

🤖 Generated with Claude Code