From ce212861609568130cf6ecef91f1836ddba473c1 Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Mon, 5 Oct 2026 09:37:16 +0200
Subject: [PATCH 01/10] fix(edsl): signed Int256 storage reads in executable
 plane (G28); ERC-20 hop lemmas (G14)

- getStorage on an Int256 field binds an Int256 (ofUint256 of the word), so
  addPanic/subPanic on it resolve to the signed checked instance, matching the
  compilation model. Previously the word was Uint256 and Int256 operands were
  coerced, so int256 += with a negative operand panicked spuriously.
- Core: hopCall_success_of_ne, hopCall_scoped_callee, hopCallView_getMapping,
  hopCallView_getMapping2.
- Smoke: Int256 regression witnesses; Erc20BalanceHop (generated ERC-20 read
  and transfer through linked_contracts).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 Contracts/Smoke.lean                 |   1 +
 Contracts/Smoke/Arithmetic.lean      |  28 ++++++
 Contracts/Smoke/Erc20BalanceHop.lean | 133 +++++++++++++++++++++++++++
 Verity/Core.lean                     |  52 +++++++++++
 Verity/Macro/Translate.lean          |  10 ++
 5 files changed, 224 insertions(+)
 create mode 100644 Contracts/Smoke/Erc20BalanceHop.lean

diff --git a/Contracts/Smoke.lean b/Contracts/Smoke.lean
index ce69823c0b..6a97c53b8f 100644
--- a/Contracts/Smoke.lean
+++ b/Contracts/Smoke.lean
@@ -30,3 +30,4 @@ import Contracts.Smoke.ParetoSmallFidelityGaps
 import Contracts.Smoke.LinkedGettersAndDeferred
 import Contracts.Smoke.HopContextAndMutableTuples
 import Contracts.Smoke.LinkedRuntimeTarget
+import Contracts.Smoke.Erc20BalanceHop
diff --git a/Contracts/Smoke/Arithmetic.lean b/Contracts/Smoke/Arithmetic.lean
index bb2793bf90..102c99b10c 100644
--- a/Contracts/Smoke/Arithmetic.lean
+++ b/Contracts/Smoke/Arithmetic.lean
@@ -284,6 +284,34 @@ verity_contract Int256CheckedSmoke where
 
 #check_contract Int256CheckedSmoke
 
+-- G28 regression: an `Int256` storage read feeds the *signed* checked add in
+-- the executable plane. Before the fix `getStorage last` bound a raw `Uint256`
+-- word, so `addPanic current delta` used unsigned `addPanic` and reverted on
+-- `-1 + 25` (the words wrap mod 2^256) while Solidity `int256 +=` succeeds.
+private def okB {α : Type} : ContractResult α → Bool
+  | .success _ _ => true
+  | .revert _ _ => false
+
+private def slot0After {α : Type} : ContractResult α → Uint256
+  | .success _ s => s.readSlot 0
+  | .revert _ s => s.readSlot 0
+
+private def int256MinusOneState : ContractState :=
+  Verity.defaultState.writeSlot 0 (Verity.Core.Uint256.ofNat (2 ^ 256 - 1))
+
+example :
+    ((Int256CheckedSmoke.applyDelta (Verity.Core.Int256.ofInt 25)).run int256MinusOneState |> okB) = true := by decide +kernel
+
+example :
+    slot0After ((Int256CheckedSmoke.applyDelta (Verity.Core.Int256.ofInt 25)).run int256MinusOneState) = 24 := by decide +kernel
+
+-- Signed overflow still panics: `maxValue + 1`.
+private def int256MaxState : ContractState :=
+  Verity.defaultState.writeSlot 0 (Verity.Core.Uint256.ofNat (2 ^ 255 - 1))
+
+example :
+    ((Int256CheckedSmoke.applyDelta (Verity.Core.Int256.ofInt 1)).run int256MaxState |> okB) = false := by decide +kernel
+
 example : Int256CheckedSmoke.spec.fields.any (fun field =>
     field.name == "last" && field.slot == some 0 &&
       match field.ty with
diff --git a/Contracts/Smoke/Erc20BalanceHop.lean b/Contracts/Smoke/Erc20BalanceHop.lean
new file mode 100644
index 0000000000..8d40912753
--- /dev/null
+++ b/Contracts/Smoke/Erc20BalanceHop.lean
@@ -0,0 +1,133 @@
+import Contracts.Common
+import Compiler.CheckContract
+
+set_option linter.unusedVariables false
+
+/-!
+# ERC-20 balance read and transfer through a linked hop (G14)
+
+A strategy-shaped contract reads `IERC20(token).balanceOf(this)` and calls
+`transfer` on a generated ERC-20 bound by `linked_contracts`. Both run the
+token's generated body at the runtime target (`hopCallView` / `hopCall`), so:
+
+* the balance read equals the token's own `balances` entry for the strategy,
+  parked at `.scoped token (.map 0 strategy)` (general theorem
+  `held_eq_token_entry`, for every state);
+* a transfer through the hop moves the token's balances, and the next balance
+  read sees the new value (kernel witnesses);
+* the strategy's own storage is untouched by the hop.
+
+This is the shape of `strategyUnderlyingBalance >= remainingReserve`
+(Pareto CLAIM-1): the left-hand side is a token-world word, not a value
+stored by the strategy.
+-/
+
+namespace Contracts.Smoke.Erc20BalanceHop
+
+open Contracts
+open Verity hiding pure bind
+open Verity.EVM.Uint256
+
+verity_contract HopToken where
+  storage
+    balances : Address → Uint256 := slot 0
+
+  function view balanceOf (account : Address) : Uint256 := do
+    let b ← getMapping balances account
+    return b
+
+  function transfer (recipient : Address, amount : Uint256) : Bool := do
+    let sender ← msgSender
+    let fromBalance ← getMapping balances sender
+    require (fromBalance >= amount) "ERC20: transfer amount exceeds balance"
+    setMapping balances sender (sub fromBalance amount)
+    let toBalance ← getMapping balances recipient
+    setMapping balances recipient (add toBalance amount)
+    return true
+
+#check_contract HopToken
+
+verity_contract HopStrategy where
+  storage
+    reserve : Uint256 := slot 0
+
+  interfaces
+    interface IHopERC20 where
+      function balanceOf(Address) view returns (Uint256)
+      function transfer(Address, Uint256) returns (Bool)
+    end
+
+  linked_contracts
+    underlying : IHopERC20 := HopToken
+
+  function view held (_t : IHopERC20, _account : Address) : Uint256 := do
+    let v ← _t.balanceOf _account
+    return v
+
+  function reentrancy_trusted pay (_t : IHopERC20, _to : Address, _amount : Uint256) : Unit := do
+    let ok ← _t.transfer _to _amount
+    require ok "SafeERC20: ERC20 operation did not succeed"
+
+#check_contract HopStrategy
+
+/-- The typed view call elaborates to the token's generated body in a view hop. -/
+theorem held_is_hopCallView (t a : Address) :
+    HopStrategy.held t a = (do
+      let v ← Contract.hopCallView t (HopToken.balanceOf a)
+      return v) := rfl
+
+/-- For every state: reading `balanceOf(a)` on a distinct token returns the
+token's own parked `balances[a]` and leaves the caller's storage unchanged. -/
+theorem held_eq_token_entry (t a : Address) (s : ContractState) (h : s.thisAddress ≠ t) :
+    HopStrategy.held t a s =
+      ContractResult.success (s.storageWords (.scoped t.toNat (.map 0 a)))
+        { s with returndata := [] } := by
+  rw [held_is_hopCallView]
+  show (Contract.hopCallView t (HopToken.balanceOf a) >>= fun v => pure v) s = _
+  have hb : HopToken.balanceOf a = (do
+      let b ← getMapping HopToken.balances a
+      return b) := rfl
+  rw [hb]
+  show Verity.bind _ _ s = _
+  unfold Verity.bind
+  rw [Contract.hopCallView_of_ne t _ s h]
+  rfl
+
+def stratAddr : Address := (70 : Address)
+def tokenAddr : Address := (71 : Address)
+def userAddr : Address := (72 : Address)
+
+/-- Strategy at `stratAddr` with its own reserve 40; the token holds 100 for the
+strategy and 5 for the user in the token's namespace. -/
+def s0 : ContractState :=
+  ({ defaultState with thisAddress := stratAddr, sender := (1 : Address) }.withStorageWords fun k =>
+      if k == .scoped tokenAddr.toNat (.map 0 stratAddr) then 100
+      else if k == .scoped tokenAddr.toNat (.map 0 userAddr) then 5
+      else 0).writeSlot 0 40
+
+theorem held_strategy_is_100 :
+    (HopStrategy.held tokenAddr stratAddr s0).getValue? = some (100 : Uint256) := by
+  decide +kernel
+
+/-- `pay` runs the token's `transfer` with `msg.sender = strategy`. -/
+def s1 : ContractState :=
+  (HopStrategy.pay ExecutableCallContext.stub tokenAddr userAddr 30 s0).getState
+
+theorem pay_moves_token_balances :
+    s1.storageWords (.scoped tokenAddr.toNat (.map 0 stratAddr)) = 70 ∧
+    s1.storageWords (.scoped tokenAddr.toNat (.map 0 userAddr)) = 35 ∧
+    s1.readSlot 0 = 40 := by
+  decide +kernel
+
+theorem held_after_pay :
+    (HopStrategy.held tokenAddr stratAddr s1).getValue? = some (70 : Uint256) := by
+  decide +kernel
+
+/-- Over-transfer reverts inside the hop and the whole state is rolled back. -/
+theorem pay_overdraw_reverts :
+    (match HopStrategy.pay ExecutableCallContext.stub tokenAddr userAddr 101 s0 with
+      | .success _ _ => false
+      | .revert _ _ => true) = true := by
+  decide +kernel
+
+end Contracts.Smoke.Erc20BalanceHop
diff --git a/Verity/Core.lean b/Verity/Core.lean
index a746468c44..f8f1aa1a34 100644
--- a/Verity/Core.lean
+++ b/Verity/Core.lean
@@ -2396,6 +2396,47 @@ def setMapping (s : StorageSlot (Address → Uint256)) (key : Address) (value :
         state.knownAddresses slot
   } := rfl
 
+/-! ### Mapping reads and writes through a distinct-address hop (G14)
+
+An ERC-20 `balanceOf(holder)` answered by a linked token body is a
+`getMapping` run inside `Contract.hopCallView token`. The callee sees its own
+mapping world (`enterHop` loads `.scoped token`), so the value read is the
+token's parked entry `.scoped token (.map slot holder)`, and the caller's
+storage is untouched. A committed mutating hop parks every plain non-slot
+write of the callee back under `.scoped callee`. -/
+
+/-- Successful distinct-address mutating hop: the result state is `exitHop`. -/
+theorem Contract.hopCall_success_of_ne {α : Type} (callee : Address) (body : Contract α)
+    (s s' : ContractState) (v : α) (h : s.thisAddress ≠ callee)
+    (hbody : body (s.enterHop s.thisAddress callee) = ContractResult.success v s') :
+    Contract.hopCall callee body s =
+      ContractResult.success v (s.exitHop s' s.thisAddress callee) := by
+  rw [Contract.hopCall_of_ne callee body s h, hbody]
+
+/-- After a successful distinct-address hop, the callee's parked word for any
+plain non-slot key (`.map`, `.map2`, `.mapUint`, `.mapChain`, `.addr`, ...) is
+the value that key had at the end of the callee body. -/
+theorem Contract.hopCall_scoped_callee {α : Type} (callee : Address) (body : Contract α)
+    (s s' : ContractState) (v : α) (h : s.thisAddress ≠ callee)
+    (hbody : body (s.enterHop s.thisAddress callee) = ContractResult.success v s')
+    (k : StorageKey) (hk : k.isPlainNonSlot = true) :
+    ((Contract.hopCall callee body s).getState).storageWords (.scoped callee.toNat k) =
+      s'.storageWords k := by
+  rw [Contract.hopCall_success_of_ne callee body s s' v h hbody]
+  exact ContractState.exitHop_scoped_callee s s' s.thisAddress callee k hk
+
+/-- `balanceOf`-shaped view hop: reading `slot[key]` inside
+`hopCallView callee` returns the callee's parked mapping entry and leaves the
+caller's state unchanged except for the cleared returndata. -/
+theorem Contract.hopCallView_getMapping (callee : Address)
+    (slot : StorageSlot (Address → Uint256)) (key : Address)
+    (s : ContractState) (h : s.thisAddress ≠ callee) :
+    Contract.hopCallView callee (getMapping slot key) s =
+      ContractResult.success (s.storageWords (.scoped callee.toNat (.map slot.slot key)))
+        { s with returndata := [] } := by
+  rw [Contract.hopCallView_of_ne callee _ s h]
+  rfl
+
 -- Typed address-valued mapping helpers on top of the word-backed storage model.
 def getMappingAddr (s : StorageSlot (Address → Uint256)) (key : Address) : Contract Address :=
   fun state => ContractResult.success (wordToAddress (state.readMap s.slot key)) state
@@ -2417,6 +2458,17 @@ def setMappingAddr (s : StorageSlot (Address → Uint256)) (key value : Address)
 def getMapping2 (s : StorageSlot (Address → Address → Uint256)) (key1 key2 : Address) : Contract Uint256 :=
   fun state => ContractResult.success (state.readMap2 s.slot key1 key2) state
 
+/-- Same as `hopCallView_getMapping` for the `getMapping2` (allowance) channel. -/
+theorem Contract.hopCallView_getMapping2 (callee : Address)
+    (slot : StorageSlot (Address → Address → Uint256)) (key1 key2 : Address)
+    (s : ContractState) (h : s.thisAddress ≠ callee) :
+    Contract.hopCallView callee (getMapping2 slot key1 key2) s =
+      ContractResult.success
+        (s.storageWords (.scoped callee.toNat (.map2 slot.slot key1 key2)))
+        { s with returndata := [] } := by
+  rw [Contract.hopCallView_of_ne callee _ s h]
+  rfl
+
 def setMapping2 (s : StorageSlot (Address → Address → Uint256)) (key1 key2 : Address) (value : Uint256) : Contract Unit :=
   fun state => ContractResult.success () (state.writeMap2 s.slot key1 key2 value)
 
diff --git a/Verity/Macro/Translate.lean b/Verity/Macro/Translate.lean
index 785f7a4959..02e62b5a1b 100644
--- a/Verity/Macro/Translate.lean
+++ b/Verity/Macro/Translate.lean
@@ -2258,6 +2258,16 @@ private partial def rewriteForEachExecutableDoElem
               let read ←
                 `(_root_.Verity.getPackedStorage $field:ident $(natTerm offset) $(natTerm width))
               pure (#[← `(doElem| let $name:ident ← $read:term)], locals)
+          -- `Int256` fields are stored as raw words (`StorageSlot Uint256`).
+          -- Reinterpret the word as `Int256` so that later checked arithmetic
+          -- (`addPanic cur delta`, ...) resolves to the signed instance, as in
+          -- the compilation model, instead of the unsigned one through the
+          -- `Int256 → Uint256` coercion (G28).
+          | some { ty := .scalar .int256, isTransient := false, packedBits := none, .. } =>
+              pure (#[← `(doElem| let $name:ident ← do
+                let word ← _root_.Verity.getStorage $field:ident
+                pure (_root_.Verity.Core.Int256.ofUint256 word))],
+                locals.push (mkTypedLocal (toString name.getId) .int256))
           | _ => pure (#[elem], locals)
       | `(term| getMappingN $field:ident $keys:term) =>
           -- Transient mapping chains read the EIP-1153 channel in the

From af94be1a850a0c15aa6f3c3f48afe5946f28aa50 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]" <github-actions[bot]@users.noreply.github.com>
Date: Mon, 5 Oct 2026 09:38:52 +0200
Subject: [PATCH 02/10] chore: auto-refresh derived artifacts

---
 artifacts/verification_status.json | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/artifacts/verification_status.json b/artifacts/verification_status.json
index 2b67547992..4e723041ea 100644
--- a/artifacts/verification_status.json
+++ b/artifacts/verification_status.json
@@ -1,6 +1,6 @@
 {
   "codebase": {
-    "core_lines": 2813,
+    "core_lines": 2865,
     "example_contracts": 19
   },
   "proofs": {

From 5076d5302f7fbe1790779c159ef5ae4cf5d69a4c Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Mon, 5 Oct 2026 10:08:34 +0200
Subject: [PATCH 03/10] test: G2 kernel evaluation of hashed-mapping bodies;
 fix ERC-20 hop smoke state

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 Contracts/Smoke/Erc20BalanceHop.lean |  4 ++--
 Contracts/Smoke/HashedMappings.lean  | 25 +++++++++++++++++++++++++
 2 files changed, 27 insertions(+), 2 deletions(-)

diff --git a/Contracts/Smoke/Erc20BalanceHop.lean b/Contracts/Smoke/Erc20BalanceHop.lean
index 8d40912753..e0379f3634 100644
--- a/Contracts/Smoke/Erc20BalanceHop.lean
+++ b/Contracts/Smoke/Erc20BalanceHop.lean
@@ -101,8 +101,8 @@ def userAddr : Address := (72 : Address)
 strategy and 5 for the user in the token's namespace. -/
 def s0 : ContractState :=
   ({ defaultState with thisAddress := stratAddr, sender := (1 : Address) }.withStorageWords fun k =>
-      if k == .scoped tokenAddr.toNat (.map 0 stratAddr) then 100
-      else if k == .scoped tokenAddr.toNat (.map 0 userAddr) then 5
+      if k == StorageKey.scoped tokenAddr.toNat (.map 0 stratAddr) then 100
+      else if k == StorageKey.scoped tokenAddr.toNat (.map 0 userAddr) then 5
       else 0).writeSlot 0 40
 
 theorem held_strategy_is_100 :
diff --git a/Contracts/Smoke/HashedMappings.lean b/Contracts/Smoke/HashedMappings.lean
index fac2b719e2..77604f380d 100644
--- a/Contracts/Smoke/HashedMappings.lean
+++ b/Contracts/Smoke/HashedMappings.lean
@@ -183,4 +183,29 @@ theorem hop_setRequest_frame (s : ContractState) (callee user : Address)
   exact ContractState.readMapChain_exitHop_enterHop_of_frame _ _ _ _ _ _ _
     (ContractState.storageWords_scoped_writeMapChain _ _ _ _ _ _ _)
 
+/-! ## Kernel evaluation of generated bodies (G2 residual)
+
+No executable accessor reaches keccak: nested / struct mappings live on the
+symbolic `mapChain` channel, single-key mappings on `.map` / `.mapUint` /
+`.map2`, and selectors are hashed at elaboration time. So whole generated
+bodies over hashed storage reduce in the kernel (`decide +kernel`), with no
+`native_decide` and no keccak evaluation. Only the *interpretation* layer
+(`mappingChainSlotLocation`, `solidityMappingSlot`, `@[implemented_by]`
+over a well-founded sponge) is not kernel-reducible; it is never on an
+execution path. -/
+
+private def g2User : Address := (0xabc : Address)
+
+private def g2Run : ContractResult (Uint256 × Uint256 × Uint256) :=
+  (do
+    HashedMappingExecSmoke.setRequest g2User 7 1000
+    HashedMappingExecSmoke.setReceipt g2User 55 3
+    let r ← HashedMappingExecSmoke.requestOf g2User 7
+    let other ← HashedMappingExecSmoke.requestOf g2User 8
+    let (p, e) ← HashedMappingExecSmoke.receiptOf g2User
+    return (r, other, p + e) : Contract _).run Verity.defaultState
+
+example : g2Run.getValue? = some ((1000 : Uint256), (0 : Uint256), (58 : Uint256)) := by
+  decide +kernel
+
 end Contracts.Smoke

From bb3b50ba2df3c56f4dca068b21a4598ef17c5a0a Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Mon, 5 Oct 2026 10:14:30 +0200
Subject: [PATCH 04/10] chore: macro property-test artifacts for ERC-20 hop
 smoke

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 .../PropertyHopStrategy.t.sol                 | 35 ++++++++++++++++
 .../PropertyHopToken.t.sol                    | 40 +++++++++++++++++++
 2 files changed, 75 insertions(+)
 create mode 100644 artifacts/macro_property_tests/PropertyHopStrategy.t.sol
 create mode 100644 artifacts/macro_property_tests/PropertyHopToken.t.sol

diff --git a/artifacts/macro_property_tests/PropertyHopStrategy.t.sol b/artifacts/macro_property_tests/PropertyHopStrategy.t.sol
new file mode 100644
index 0000000000..081743a274
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyHopStrategy.t.sol
@@ -0,0 +1,35 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyHopStrategyTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/Erc20BalanceHop.lean
+ */
+contract PropertyHopStrategyTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYul("HopStrategy");
+        require(target != address(0), "Deploy failed");
+    }
+
+    // Property 1: TODO decode and assert `held` result
+    function testTODO_Held_DecodeAndAssert() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("held(address,address)", alice, alice));
+        require(ok, "held reverted unexpectedly");
+        assertEq(ret.length, 32, "held ABI return length mismatch (expected 32 bytes)");
+        // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
+        ret;
+    }
+    // Property 2: pay has no unexpected revert
+    function testAuto_Pay_NoUnexpectedRevert() public {
+        vm.prank(alice);
+        (bool ok,) = target.call(abi.encodeWithSignature("pay(address,address,uint256)", alice, alice, uint256(1)));
+        require(ok, "pay reverted unexpectedly");
+    }
+}
diff --git a/artifacts/macro_property_tests/PropertyHopToken.t.sol b/artifacts/macro_property_tests/PropertyHopToken.t.sol
new file mode 100644
index 0000000000..d7ac61cd3f
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyHopToken.t.sol
@@ -0,0 +1,40 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyHopTokenTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/Erc20BalanceHop.lean
+ */
+contract PropertyHopTokenTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYul("HopToken");
+        require(target != address(0), "Deploy failed");
+    }
+
+    // Property 1: balanceOf reads the configured mapping value
+    function testAuto_BalanceOf_ReadsConfiguredMapping() public {
+        uint256 expected = uint256(1);
+        vm.store(target, _mappingSlot(bytes32(uint256(uint160(alice))), 0), bytes32(uint256(expected)));
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("balanceOf(address)", alice));
+        require(ok, "balanceOf reverted unexpectedly");
+        assertEq(ret.length, 32, "balanceOf ABI return length mismatch (expected 32 bytes)");
+        uint256 actual = abi.decode(ret, (uint256));
+        assertEq(actual, expected, "balanceOf should decode the configured mapping value");
+    }
+    // Property 2: TODO decode and assert `transfer` result
+    function testTODO_Transfer_DecodeAndAssert() public {
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("transfer(address,uint256)", alice, uint256(1)));
+        require(ok, "transfer reverted unexpectedly");
+        assertEq(ret.length, 32, "transfer ABI return length mismatch (expected 32 bytes)");
+        // TODO(#1011): decode `ret` and assert the concrete postcondition from Lean theorem.
+        ret;
+    }
+}

From 9422010693c1280abfa95d50400219f18e90b188 Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Mon, 5 Oct 2026 10:43:50 +0200
Subject: [PATCH 05/10] docs: executable Int256 storage reads are signed (G28)

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 docs/PARETO_MODEL_SUPPORT.md | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/docs/PARETO_MODEL_SUPPORT.md b/docs/PARETO_MODEL_SUPPORT.md
index 0bf8ad6fe7..556845132a 100644
--- a/docs/PARETO_MODEL_SUPPORT.md
+++ b/docs/PARETO_MODEL_SUPPORT.md
@@ -44,7 +44,13 @@ pattern is the bit-reinterpretation already provided by `toUint256`.
 `FieldType.int256` (one EVM word, layout-identical to `uint256`) so the
 field round-trips through `Storage.lean`, layout reports, and
 `#check_contract`. The executable slot remains a `Uint256` word; the DSL
-and compilation model keep the signed tag.
+and compilation model keep the signed tag. In the executable plane
+`let x ← getStorage f` on an unpacked persistent `Int256` field binds
+`Int256.ofUint256 word`, so later `addPanic`/`subPanic`/... resolve to the
+signed instances exactly as in the compilation model (G28: before, `x` was
+the raw `Uint256` word and `addPanic x delta` silently used the unsigned
+check through the `Int256 → Uint256` coercion, reverting on valid
+`int256 +=` with a negative operand and missing real signed overflow).
 
 **Compilation model.** Bound `let x ← addPanic a b` with `Int256`
 operands lowers to wrapping `add`/`sub`/`mul` plus an `slt`-based overflow

From 732794653cb236731bdc368aaf0c2b3f17695d39 Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Mon, 5 Oct 2026 10:13:12 +0200
Subject: [PATCH 06/10] feat(edsl): executable constructor for ordinary
 verity_contract (verity#2465, G29 part)

Ordinary contracts now get an executable `constructor` definition, like
mixins and include hosts already did, so a deployment boundary can run the
generated constructor body. Best effort: if the body has no executable
lowering, elaboration state is restored and only the compilation-model
constructor is kept (no new failures for existing contracts).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 Contracts/Smoke.lean                       |  1 +
 Contracts/Smoke/ConstructorExecutable.lean | 53 ++++++++++++++++++++++
 Verity/Macro/Elaborate.lean                | 20 ++++++++
 3 files changed, 74 insertions(+)
 create mode 100644 Contracts/Smoke/ConstructorExecutable.lean

diff --git a/Contracts/Smoke.lean b/Contracts/Smoke.lean
index 6a97c53b8f..1e8f1185da 100644
--- a/Contracts/Smoke.lean
+++ b/Contracts/Smoke.lean
@@ -31,3 +31,4 @@ import Contracts.Smoke.LinkedGettersAndDeferred
 import Contracts.Smoke.HopContextAndMutableTuples
 import Contracts.Smoke.LinkedRuntimeTarget
 import Contracts.Smoke.Erc20BalanceHop
+import Contracts.Smoke.ConstructorExecutable
diff --git a/Contracts/Smoke/ConstructorExecutable.lean b/Contracts/Smoke/ConstructorExecutable.lean
new file mode 100644
index 0000000000..081973db32
--- /dev/null
+++ b/Contracts/Smoke/ConstructorExecutable.lean
@@ -0,0 +1,53 @@
+import Contracts.Common
+
+/-!
+# Executable constructors for ordinary contracts (verity#2465, Pareto G29)
+
+An ordinary `verity_contract` constructor now has an executable
+`.constructor` definition (previously only mixins and include hosts did), so a
+deployment boundary can run the generated constructor body. Constructors
+whose body has no executable lowering (here: `String` parameters) still
+elaborate and keep only the compilation-model constructor.
+-/
+
+namespace Contracts.Smoke.ConstructorExecutable
+
+open Contracts
+open Verity hiding pure bind
+open Verity.EVM.Uint256
+
+verity_contract CtorExec where
+  storage
+    supply : Uint256 := slot 0
+    minter : Address := slot 5
+
+  constructor (initial : Uint256) := do
+    let sender ← msgSender
+    setStorageAddr minter sender
+    setStorage supply initial
+
+  function view minterOf () : Address := do
+    let m ← getStorageAddr minter
+    return m
+
+#check (CtorExec.constructor : Uint256 → Contract Unit)
+
+private def deployer : Address := (0x1234 : Address)
+
+private def deployed : ContractState :=
+  ((CtorExec.constructor 77).run { Verity.defaultState with sender := deployer }).getState
+
+example : deployed.readAddrSlot 5 = deployer ∧ deployed.readSlot 0 = 77 := by
+  decide +kernel
+
+-- A constructor with metadata `String` parameters still elaborates.
+verity_contract CtorWithStrings where
+  storage
+    decimalsSlot : Uint256 := slot 0
+
+  constructor (_name : String, _symbol : String) := do
+    setStorage decimalsSlot 18
+
+example : CtorWithStrings.spec.constructor.isSome = true := by decide
+
+end Contracts.Smoke.ConstructorExecutable
diff --git a/Verity/Macro/Elaborate.lean b/Verity/Macro/Elaborate.lean
index 62c913b122..0eddbdb9da 100644
--- a/Verity/Macro/Elaborate.lean
+++ b/Verity/Macro/Elaborate.lean
@@ -200,6 +200,26 @@ private def elabVerityContractOrMixin (stx : Syntax) : CommandElabM Unit := do
             (linkedContracts := parsed.linkedContracts))
       | none => pure ()
 
+    -- Ordinary contracts also get an executable `constructor` (verity#2465),
+    -- so a creation boundary can run the generated constructor body instead
+    -- of a hand-extracted helper. Best effort: a constructor whose body has
+    -- no executable lowering (e.g. `String` parameters) keeps the previous
+    -- behaviour (compilation model only) instead of failing elaboration.
+    if !isMixin && resolvedIncludes.isEmpty then
+      match ctor with
+      | some ctorDecl =>
+          let saved ← get
+          let hadErrors := saved.messages.hasErrors
+          try
+            elabCommand (← mkConstructorDefCommandPublic translationFields translationErrorDecls
+              translationConstDecls translationImmutableDecls translationExternalDecls
+              translationFunctions ctorDecl (linkedContracts := parsed.linkedContracts))
+            if (← get).messages.hasErrors && !hadErrors then
+              set saved
+          catch _ =>
+            set saved
+      | none => pure ()
+
     let specName : Ident :=
       if resolvedIncludes.isEmpty then mkIdent (Name.mkSimple "spec")
       else mkIdent (Name.mkSimple "host_spec")

From e46bfbacc6f536e97e377e8975b9492a29572c95 Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Mon, 5 Oct 2026 10:43:15 +0200
Subject: [PATCH 07/10] G29: use generated ERC721 constructor; ctor smoke
 kernel witnesses; property artifacts

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 Contracts/ERC721/ERC721.lean                  |  5 +--
 Contracts/Smoke/ConstructorExecutable.lean    | 13 +++++---
 .../PropertyCtorExec.t.sol                    | 31 +++++++++++++++++++
 .../PropertyCtorWithStrings.t.sol             | 20 ++++++++++++
 4 files changed, 61 insertions(+), 8 deletions(-)
 create mode 100644 artifacts/macro_property_tests/PropertyCtorExec.t.sol
 create mode 100644 artifacts/macro_property_tests/PropertyCtorWithStrings.t.sol

diff --git a/Contracts/ERC721/ERC721.lean b/Contracts/ERC721/ERC721.lean
index 67779eacd6..1fd5c485b0 100644
--- a/Contracts/ERC721/ERC721.lean
+++ b/Contracts/ERC721/ERC721.lean
@@ -108,10 +108,7 @@ verity_contract ERC721 where
 
 namespace ERC721
 
-def «constructor» (initialOwner : Address) : Contract Unit := do
-  setStorageAddr owner initialOwner
-  setStorage totalSupply 0
-  setStorage nextTokenId 0
+-- `constructor` is generated by `verity_contract` (verity#2465).
 
 abbrev boolToWord : Bool → Uint256 := Contracts.boolToWord
 
diff --git a/Contracts/Smoke/ConstructorExecutable.lean b/Contracts/Smoke/ConstructorExecutable.lean
index 081973db32..cd42c0eb4f 100644
--- a/Contracts/Smoke/ConstructorExecutable.lean
+++ b/Contracts/Smoke/ConstructorExecutable.lean
@@ -6,8 +6,8 @@ import Contracts.Common
 An ordinary `verity_contract` constructor now has an executable
 `.constructor` definition (previously only mixins and include hosts did), so a
 deployment boundary can run the generated constructor body. Constructors
-whose body has no executable lowering (here: `String` parameters) still
-elaborate and keep only the compilation-model constructor.
+whose body has no executable lowering still elaborate and keep only the
+compilation-model constructor.
 -/
 
 namespace Contracts.Smoke.ConstructorExecutable
@@ -40,7 +40,8 @@ private def deployed : ContractState :=
 example : deployed.readAddrSlot 5 = deployer ∧ deployed.readSlot 0 = 77 := by
   decide +kernel
 
--- A constructor with metadata `String` parameters still elaborates.
+-- Tranche-shaped constructor with metadata `String` parameters (the strings
+-- are accepted as executable parameters; `String` storage stays unsupported).
 verity_contract CtorWithStrings where
   storage
     decimalsSlot : Uint256 := slot 0
@@ -48,6 +49,10 @@ verity_contract CtorWithStrings where
   constructor (_name : String, _symbol : String) := do
     setStorage decimalsSlot 18
 
-example : CtorWithStrings.spec.constructor.isSome = true := by decide
+#check (CtorWithStrings.constructor : String → String → Contract Unit)
+
+example :
+    (((CtorWithStrings.constructor "AA" "AA_T").run Verity.defaultState).getState).readSlot 0 = 18 := by
+  decide +kernel
 
 end Contracts.Smoke.ConstructorExecutable
diff --git a/artifacts/macro_property_tests/PropertyCtorExec.t.sol b/artifacts/macro_property_tests/PropertyCtorExec.t.sol
new file mode 100644
index 0000000000..5e75b84f04
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyCtorExec.t.sol
@@ -0,0 +1,31 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyCtorExecTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/ConstructorExecutable.lean
+ */
+contract PropertyCtorExecTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYulWithArgs("CtorExec", abi.encode(uint256(1)));
+        require(target != address(0), "Deploy failed");
+    }
+
+    // Property 1: minterOf reads storage slot 5 and decodes the result
+    function testAuto_MinterOf_ReadsConfiguredStorage() public {
+        address expected = alice;
+        vm.store(target, bytes32(uint256(5)), bytes32(uint256(uint160(expected))));
+        vm.prank(alice);
+        (bool ok, bytes memory ret) = target.call(abi.encodeWithSignature("minterOf()"));
+        require(ok, "minterOf reverted unexpectedly");
+        assertEq(ret.length, 32, "minterOf ABI return length mismatch (expected 32 bytes)");
+        address actual = abi.decode(ret, (address));
+        assertEq(actual, expected, "minterOf should return storage slot 5");
+    }
+}
diff --git a/artifacts/macro_property_tests/PropertyCtorWithStrings.t.sol b/artifacts/macro_property_tests/PropertyCtorWithStrings.t.sol
new file mode 100644
index 0000000000..fc49c7c298
--- /dev/null
+++ b/artifacts/macro_property_tests/PropertyCtorWithStrings.t.sol
@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: MIT
+pragma solidity ^0.8.33;
+
+import "./yul/YulTestBase.sol";
+
+/**
+ * @title PropertyCtorWithStringsTest
+ * @notice Auto-generated baseline property stubs from `verity_contract` declarations.
+ * @dev Source: Contracts/Smoke/ConstructorExecutable.lean
+ */
+contract PropertyCtorWithStringsTest is YulTestBase {
+    address target;
+    address alice = address(0x1111);
+
+    function setUp() public {
+        target = deployYulWithArgs("CtorWithStrings", abi.encode("verity", "verity"));
+        require(target != address(0), "Deploy failed");
+    }
+
+}

From 58d5ee8dc4e55283e6023968cff01008b97e5639 Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Mon, 5 Oct 2026 10:44:34 +0200
Subject: [PATCH 08/10] ci: trigger


From 2bbbb950716ef72acc8a82639aae47df3012bab3 Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Mon, 5 Oct 2026 10:55:59 +0200
Subject: [PATCH 09/10] test: replace #check with example in ctor smoke
 (hygiene)

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 Contracts/Smoke/ConstructorExecutable.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Contracts/Smoke/ConstructorExecutable.lean b/Contracts/Smoke/ConstructorExecutable.lean
index cd42c0eb4f..f7ed914b8f 100644
--- a/Contracts/Smoke/ConstructorExecutable.lean
+++ b/Contracts/Smoke/ConstructorExecutable.lean
@@ -30,7 +30,7 @@ verity_contract CtorExec where
     let m ← getStorageAddr minter
     return m
 
-#check (CtorExec.constructor : Uint256 → Contract Unit)
+example : Uint256 → Contract Unit := CtorExec.constructor
 
 private def deployer : Address := (0x1234 : Address)
 
@@ -49,7 +49,7 @@ verity_contract CtorWithStrings where
   constructor (_name : String, _symbol : String) := do
     setStorage decimalsSlot 18
 
-#check (CtorWithStrings.constructor : String → String → Contract Unit)
+example : String → String → Contract Unit := CtorWithStrings.constructor
 
 example :
     (((CtorWithStrings.constructor "AA" "AA_T").run Verity.defaultState).getState).readSlot 0 = 18 := by

From a02b60fa69deaee87f8702fdfd6104c80e000139 Mon Sep 17 00:00:00 2001
From: Thomas Marchand <thomas@lfglabs.dev>
Date: Mon, 5 Oct 2026 13:34:03 +0200
Subject: [PATCH 10/10] fix(macro): suppress unused-param lint on generated
 executable constructor

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 Verity/Macro/Elaborate.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/Verity/Macro/Elaborate.lean b/Verity/Macro/Elaborate.lean
index 0eddbdb9da..0976d08858 100644
--- a/Verity/Macro/Elaborate.lean
+++ b/Verity/Macro/Elaborate.lean
@@ -208,6 +208,10 @@ private def elabVerityContractOrMixin (stx : Syntax) : CommandElabM Unit := do
     if !isMixin && resolvedIncludes.isEmpty then
       match ctor with
       | some ctorDecl =>
+          -- Binders get synthetic source info: the generated `def` must not
+          -- re-report unused constructor parameters on the user's source.
+          let ctorDecl := { ctorDecl with
+            params := ctorDecl.params.map fun p => { p with ident := mkIdent p.ident.getId } }
           let saved ← get
           let hadErrors := saved.messages.hasErrors
           try