G29: executable constructor for ordinary verity_contract (verity#2465)

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
 

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

Contracts/Smoke/ConstructorExecutable.lean

@@ -0,0 +1,58 @@
+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 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
+
+example : Uint256 → Contract Unit := CtorExec.constructor
+
+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
+
+-- 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
+
+  constructor (_name : String, _symbol : String) := do
+    setStorage decimalsSlot 18
+
+example : String → String → Contract Unit := CtorWithStrings.constructor
+
+example :
+    (((CtorWithStrings.constructor "AA" "AA_T").run Verity.defaultState).getState).readSlot 0 = 18 := by
+  decide +kernel
+
+end Contracts.Smoke.ConstructorExecutable

Verity/Macro/Elaborate.lean

@@ -200,6 +200,30 @@ 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 =>
+          -- 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
+            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")

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");
+    }
+}

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");
+    }
+
+}