feat(EthState): supply mathematical transaction view

.github/workflows/ci.yml

@@ -159,6 +159,16 @@ jobs:
           uv run --no-project --python 3.12 python -B -O scripts/test_pre_state_account_default_output_parser.py
           uv run --no-project --python 3.12 python -B scripts/test_pre_state_account_default_source.py
           uv run --no-project --python 3.12 python -B -O scripts/test_pre_state_account_default_source.py
+      - name: Complete mathematical transaction-view regressions
+        run: |
+          lake build transaction-view-native-tests --wfail
+          lake exe check-decls scripts.TransactionViewNativeTests
+          lake exe transaction-view-native-tests > .lake/transaction-view-native.jsonl
+          lake env lean --run scripts/TransactionViewNativeTests.lean > .lake/transaction-view-interpreted.jsonl
+          uv run --no-project --python 3.12 python -B STFSpec/Conformance/State/transaction_view_model.py --check-target .lake/transaction-view-native.jsonl
+          uv run --no-project --python 3.12 python -B STFSpec/Conformance/State/transaction_view_model.py --check-target .lake/transaction-view-interpreted.jsonl
+          uv run --no-project --python 3.12 python -B scripts/test_transaction_view_output_parser.py
+          uv run --no-project --python 3.12 python -B -O scripts/test_transaction_view_output_parser.py
       - name: Complete opaque witness ancestor regressions
         run: |
           lake build witness-ancestors-native-tests --wfail

CONTRIBUTING.md

@@ -221,6 +221,14 @@ uv run --no-project --python 3.12 python -B scripts/test_pre_state_account_outpu
 uv run --no-project --python 3.12 python -B -O scripts/test_pre_state_account_output_parser.py
 uv run --no-project --python 3.12 python -B scripts/test_pre_state_account_source.py
 uv run --no-project --python 3.12 python -B -O scripts/test_pre_state_account_source.py
+lake build transaction-view-native-tests --wfail
+lake exe check-decls scripts.TransactionViewNativeTests
+lake exe transaction-view-native-tests > .lake/transaction-view-native.jsonl
+lake env lean --run scripts/TransactionViewNativeTests.lean > .lake/transaction-view-interpreted.jsonl
+uv run --no-project --python 3.12 python -B STFSpec/Conformance/State/transaction_view_model.py --check-target .lake/transaction-view-native.jsonl
+uv run --no-project --python 3.12 python -B STFSpec/Conformance/State/transaction_view_model.py --check-target .lake/transaction-view-interpreted.jsonl
+uv run --no-project --python 3.12 python -B scripts/test_transaction_view_output_parser.py
+uv run --no-project --python 3.12 python -B -O scripts/test_transaction_view_output_parser.py
 lake build pre-state-account-default-native-tests --wfail
 lake exe check-decls scripts.PreStateAccountDefaultNativeTests
 lake exe pre-state-account-default-native-tests > .lake/pre-state-account-default-native.jsonl

STFSpec/Conformance.lean

@@ -226,6 +226,7 @@ import STFSpec.Conformance.State.ReadSetsGuards
 import STFSpec.Conformance.State.BlockExtractionCallerProofs
 import STFSpec.Conformance.State.BlockExtractionGuards
 import STFSpec.Conformance.State.BlockViewCallerProofs
+import STFSpec.Conformance.State.TransactionViewCallerProofs
 import STFSpec.Conformance.State.BlockViewGuards
 import STFSpec.Conformance.State.BlockStateGuards
 

STFSpec/Conformance/State/TransactionViewCallerProofs.lean

@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2026 The STFspec Contributors. Licensed under Apache-2.0 OR MIT.
+-/
+
+import STFSpec.State
+
+/-!
+# Public mathematical transaction-view callers
+
+Library `EthConformance`: private class-free clients use only the public account law.
+Spec guidance: `STFSpec/informal/modules/EthState.md` §§3/4/7.1/7.2.
+-/
+
+namespace STFSpec.Conformance.State.TransactionViewCallerProofs
+
+open STFSpec.State STFSpec.Base
+
+private def signature : {m : Type → Type} → MathState → TxState m → MathState :=
+  @TxState.view
+
+private theorem account {m : Type → Type} (σ : MathState) (t : TxState m) (a : Address) :
+    (t.view σ).account? a =
+      match t.rev.accountWrites[a]? with
+      | some replacement => replacement
+      | none => (t.block.view σ).account? a := TxState.view_account?_eq σ t a
+
+private theorem tombstone {m : Type → Type} (σ : MathState) (t : TxState m) (a : Address)
+    (ha : t.rev.accountWrites[a]? = some none) : (t.view σ).account? a = none := by
+  rw [TxState.view_account?_eq, ha]
+
+private theorem missing {m : Type → Type} (σ : MathState) (t : TxState m) (a : Address)
+    (ha : t.rev.accountWrites[a]? = none) :
+    (t.view σ).account? a = (t.block.view σ).account? a := by
+  rw [TxState.view_account?_eq, ha]
+
+private def Contravariant (α : Type) : Type := α → Nat
+#check_failure (inferInstance : Monad Contravariant)
+
+private def noMonadSignature : MathState → TxState Contravariant → MathState := signature
+
+private theorem noMonadLaw (σ : MathState) (t : TxState Contravariant) (a : Address) :
+    (noMonadSignature σ t).account? a =
+      match t.rev.accountWrites[a]? with
+      | some replacement => replacement
+      | none => (t.block.view σ).account? a := TxState.view_account?_eq σ t a
+
+end STFSpec.Conformance.State.TransactionViewCallerProofs