Small ergonomics found while translating ~2500 lines of Solidity into verity_contract on c907fef0:
- Namespace clashes.
emit, typed interface calls (externalStaticCallContractWordsTo, ExternalResult, ExecutableCallContext) are generated as unqualified names from the Contracts namespace, so a contract outside Contracts.* must open Contracts; that makes Int256, toInt256, toUint256, contractAddress, blockTimestamp, blockNumber ambiguous with Verity.* ("Ambiguous term Int256"). Every closure file needs open Contracts hiding Int256 toInt256 toUint256 contractAddress blockTimestamp blockNumber. Generated code should use _root_.Contracts.… qualified names.
- Reserved identifiers. Solidity parameter names
from, to and locals named this, partial fail with parser errors or (for this) a puzzling ExternalResult Uint256 type mismatch, because they are Lean keywords / the anonymous have name. A clear diagnostic ("from is reserved; rename the parameter") would help; ERC-20's _transfer(address from, address to, uint256 amount) is the canonical victim.
- Reserved helper forms.
balanceOf, allowance, totalSupply are ERC-20 helper forms; an ERC-20 contract cannot call its own allowance(owner, spender) internally (the executable rewrite treats it as the helper and produces (fun owner spender => allowance owner_ owner spender) spender type errors).
- Forward references. Functions must be declared callee-first because the executable plane emits Lean
defs in source order; Solidity files are typically ordered the other way.
Closure-side tracking: audit/VERITY-GAPS.md G12/G13/G16.
Small ergonomics found while translating ~2500 lines of Solidity into
verity_contractonc907fef0:emit, typed interface calls (externalStaticCallContractWordsTo,ExternalResult,ExecutableCallContext) are generated as unqualified names from theContractsnamespace, so a contract outsideContracts.*mustopen Contracts; that makesInt256,toInt256,toUint256,contractAddress,blockTimestamp,blockNumberambiguous withVerity.*("Ambiguous term Int256"). Every closure file needsopen Contracts hiding Int256 toInt256 toUint256 contractAddress blockTimestamp blockNumber. Generated code should use_root_.Contracts.…qualified names.from,toand locals namedthis,partialfail with parser errors or (forthis) a puzzlingExternalResult Uint256type mismatch, because they are Lean keywords / the anonymoushavename. A clear diagnostic ("fromis reserved; rename the parameter") would help; ERC-20's_transfer(address from, address to, uint256 amount)is the canonical victim.balanceOf,allowance,totalSupplyare ERC-20 helper forms; an ERC-20 contract cannot call its ownallowance(owner, spender)internally (the executable rewrite treats it as the helper and produces(fun owner spender => allowance owner_ owner spender) spendertype errors).defs in source order; Solidity files are typically ordered the other way.Closure-side tracking:
audit/VERITY-GAPS.mdG12/G13/G16.