Repository navigation
Initialization transcription: contract creation and internal String helpers unsupported at 600014d5 #2465
Description
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 bimport 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 deployedObserved 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.constructorObserved: Unknown identifier MIConstructorExecutable.constructor at the same pin. Expected: an executable constructor declaration, usable from the deferred creation boundary.
Activity
Th0rgal commentedon Oct 5, 2026
Scope update for Pareto G29 (2026-10-05)
Status against Verity main
85e0262b(identical to the pin600014d5for every part of this issue):C.constructorfor ordinaryverity_contract#check MIConstructorExecutable.constructor→ unknown identifierfix/pareto-g29-ctor(stacked on #2469): ordinary contracts now emit an executableconstructor.Stringparameters are accepted, e.g.CtorWithStrings.constructor : String → String → Contract UnitinContracts/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 sourceDeploy.lean: "unsupported bind source"keccak256(rlp(sender, nonce)), a nonce channel, code installation, and the failure / out-of-gas branch.Stringparams/result (_concat,abi.encodePacked)Concat.lean: "helper call '_concat' uses a parameter or return type..."StringstorageMacro/Storage.lean/Translate.lean(storage field cannot be String)What is sound today, and what a consumer must assume
Sound:
linked_contracts ... := deferredcreation boundary whose responder runs the generated constructor body (nowC.constructordirectly) inContract.hopCallat an environment-supplied address.Must be stated as assumptions:
name/symbolstrings 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.