Skip to content

Ergonomics: Contracts namespace clashes, reserved identifiers (from/to/this), reserved ERC-20 helper names, callee-first ordering #2423

Description

@Th0rgal

Small ergonomics found while translating ~2500 lines of Solidity into verity_contract on c907fef0:

  1. 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.
  2. 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.
  3. 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).
  4. 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.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions