Initialization transcription: contract creation and internal String helpers unsupported at 600014d5

[Th0rgal]

At Verity pin 600014d5be3ece57be639d8ec617b9c4736d02cd, the Pareto initialization transcription needs Solidity new IdleCDOTranche(name, symbol) and internal string helpers (string(abi.encodePacked(a, b))). The macro rejects both minimal shapes below. String storage is also explicitly rejected by Verity/Macro/Storage.lean, so metadata initialization cannot currently be transcribed directly.

These are needed by idle-tranches 54502d1, IdleCDOCreditVault.sol L434-435 and L618-619, and IdleCreditVault.sol L150-154. Lean toolchain: v4.31.0. The Verity pin must remain fixed for this audit.

Reproduce with lake env lean Concat.lean and lake env lean Deploy.lean in a project requiring this pin.

import Contracts.Common

open Verity hiding pure bind

-- IdleCDOCreditVault.sol L618-619: string(abi.encodePacked(a, b)).
verity_contract MIConcat where
  storage

  function internal pure _concat (a : String, b : String) : String := do
    return String.append a b

import Contracts.Common

open Verity hiding pure bind

-- Minimal deployment shape needed by IdleCDOCreditVault.sol L434-435.
verity_contract MITranche where
  storage

  constructor (name_ : String, symbol_ : String) := do
    pure ()

verity_contract MIDeploy where
  storage

  function internal _deployTranche (name_ : String, symbol_ : String) : Address := do
    let deployed ← new MITranche name_ symbol_
    return deployed

Observed diagnostics:

Concat.lean:9:25: error: helper call '_concat' uses a parameter or return type that direct macro helper lowering does not support yet; only static non-fallback/non-receive helpers can be lowered to internal specs
Deploy.lean:16:19: error: unsupported bind source; expected getStorage/getStorageAddr/getStorageArrayLength/getStorageArrayElement/getMapping/getMappingAddr/getMappingUint/getMappingUintAddr/getMappingWord/getMapping2/getMappingN/structMember/structMember2/msgSender/msgValue/selfBalance/tload/ecrecover/ecmCall, a direct internal helper call, or a qualified library helper call

Expected: a supported DSL spelling with executable semantics for contract creation and string concatenation/metadata, or a documented faithful external/deferred boundary for deployment. The audit will use existing linked_contracts / deferred boundaries where possible and record the modelling limits, without repinning or hand-writing replacement state transitions.

One further creation-boundary limitation: ordinary verity_contract constructors are included in the compilation model but do not get an executable .constructor declaration. A direct generated executable body is emitted only for mixins and include-expanded hosts (Macro/Elaborate.lean around L181-195). The audit extracts the source constructor body as an internal DSL helper and makes the constructor delegate to it, so the deferred creation responder can call that same generated body without handwritten storage writes.

Minimal repro:

import Contracts.Common
open Verity hiding pure bind
verity_contract MIConstructorExecutable where
  storage
    minter : Address := slot 5
  constructor () := do
    let sender ← msgSender
    setStorageAddr minter sender
#check MIConstructorExecutable.constructor

Observed: Unknown identifier MIConstructorExecutable.constructor at the same pin. Expected: an executable constructor declaration, usable from the deferred creation boundary.

[Th0rgal]

Scope update for Pareto G29 (2026-10-05)

Status against Verity main 85e0262b (identical to the pin 600014d5 for every part of this issue):

Item	Repro on main	Status
Executable C.constructor for ordinary verity_contract	#check MIConstructorExecutable.constructor → unknown identifier	FIXED on branch fix/pareto-g29-ctor (stacked on #2469): ordinary contracts now emit an executable constructor. String parameters are accepted, e.g. CtorWithStrings.constructor : String → String → Contract Unit in Contracts/Smoke/ConstructorExecutable.lean, with kernel witnesses. If a constructor body has no executable lowering, elaboration falls back to the previous behaviour (compilation-model constructor only) instead of failing.
new C(args) (CREATE) as a bind source	Deploy.lean: "unsupported bind source"	Not fixed (out of scope). It needs a CREATE semantics in the executable plane: address derivation keccak256(rlp(sender, nonce)), a nonce channel, code installation, and the failure / out-of-gas branch.
Internal helper with String params/result (_concat, abi.encodePacked)	Concat.lean: "helper call '_concat' uses a parameter or return type..."	Not fixed (out of scope). It needs dynamic-bytes values in internal specs.
String storage	rejected in Macro/Storage.lean / Translate.lean (storage field cannot be String)	Not fixed (out of scope).

What is sound today, and what a consumer must assume

Sound:

• A linked_contracts ... := deferred creation boundary whose responder runs the generated constructor body (now C.constructor directly) in Contract.hopCall at an environment-supplied address.
• The storage effects of initialization are therefore generated bodies, not hand-written transitions.

Must be stated as assumptions:

1. Freshness. Deployed addresses are fresh and distinct from every existing contract or account the model reads. CREATE address derivation is not modelled, so no guarantee may depend on the concrete address value.
2. Code identity. The code at the new address is the generated contract (no CREATE failure, no out-of-gas, no pre-existing code).
3. Metadata. name / symbol strings and their concatenation are not modelled (they are erased). No guarantee may depend on metadata.

Leaving this issue open for the CREATE and String items.