Skip to content

README.md

Latest commit

 

History

History
124 lines (99 loc) · 5.71 KB

README.md

File metadata and controls

124 lines (99 loc) · 5.71 KB

Standard External Call Modules

This directory contains Verity's standard ECM (External Call Module) library. Each module packages a reusable external call pattern as a typed, auditable Lean structure that the compiler can plug in without modification.

Available Modules

File Modules Replaces
ERC20.lean safeTransfer, safeTransferFrom, safeApprove, solmateSafeTransfer, solmateSafeTransferFrom, balanceOf, allowance, totalSupply OpenZeppelin-style and Solmate-style optional-return write wrappers plus canonical ERC-20 read wrappers
ERC4626.lean previewDeposit, previewMint, previewWithdraw, previewRedeem, convertToAssets, convertToShares, totalAssets, asset, maxDeposit, maxMint, maxWithdraw, maxRedeem, deposit canonical vault preview/conversion wrappers plus a standard deposit wrapper
Hashing.lean abiEncodeStaticWords, abiEncodePackedWords / abiEncodePacked, sha256PackedWords / sha256Packed, abiEncodePackedStaticSegments, sha256PackedStaticSegments, eip712Digest handwritten static ABI, packed, and EIP-712 hash preimage mstore choreography
Oracle.lean oracleReadUint256 canonical oracle read wrappers
Precompiles.lean ecrecover, sha256Memory / sha256, bn256Add, bn256ScalarMul, bn256Pairing Stmt.ecrecover, handwritten SHA-256 / BN254 (alt_bn128) precompile calls
Callbacks.lean callback Stmt.callback
Calls.lean withReturn, callWithValue, callWithValueBytes, bubblingValueCall, bubblingValueCallNoOutput Stmt.externalCallWithReturn; generic call{value:v} adapter calls; handwritten low-level call{value: ...} wrappers
Create2SSTORE2.lean create2Deploy, sstore2ReadCode handwritten CREATE2 deployment and SSTORE2-style extcodecopy code-as-data reads

Usage

import Compiler.Modules.ERC20

-- In a function body:
body := [
  Modules.ERC20.safeTransfer
    (Expr.storage "token")
    (Expr.param "to")
    (Expr.param "amount"),
  Stmt.stop
]

Choose the ERC-20 write wrapper whose optional-return policy matches the Solidity source. safeTransfer / safeTransferFrom / safeApprove use OpenZeppelin-style code-existence and exact-bool checks; solmateSafeTransfer and solmateSafeTransferFrom match Solmate SafeTransferLib's returndatasize() == 0 || (returndatasize() > 31 && mload(ptr) == 1) shape.

Static-word packed hashing helpers are available for ZK/audit preimages whose items are already 32-byte words:

Modules.Hashing.abiEncodeStaticWords
  "digest"
  [Expr.param "marketId", Expr.param "assets", Expr.param "shares"]

Modules.Hashing.abiEncodePackedWords
  "digest"
  [Expr.param "root", Expr.param "contextHash", Expr.param "nullifier"]

Modules.Hashing.sha256PackedWords
  "publicSignalDigest"
  [Expr.param "root", Expr.param "contextHash"]

Use abiEncodeStaticWords for the static-word subset of keccak256(abi.encode(...)). The shorter Modules.Hashing.abiEncodePacked and Modules.Hashing.sha256Packed aliases are available for the same static-word packed semantics as abiEncodePackedWords and sha256PackedWords. These helpers write words contiguously at the Solidity free-memory pointer. For static packed preimages with byte-width segments such as address-sized values, use the segment helpers:

Modules.Hashing.abiEncodePackedStaticSegments
  "digest"
  [(Expr.param "who", 20), (Expr.param "amount", 32)]

Modules.Hashing.sha256PackedStaticSegments
  "publicSignalDigest"
  [(Expr.param "who", 20), (Expr.param "contextHash", 32)]

Segment widths are explicit byte counts from 1 to 32. Sub-word values are masked to their requested width and left-aligned before mstore, and subsequent segments are placed at byte-precise offsets. These helpers still do not implement dynamic Solidity packed encoding for bytes or string.

For EIP-712's final typed-data digest, use:

Modules.Hashing.eip712Digest
  "digest"
  (Expr.param "domainSeparator")
  (Expr.param "structHash")

This helper fixes the hex"1901" || domainSeparator || structHash preimage; domain separator and struct hash construction remain explicit model code.

Writing a New Standard Module

  1. Create Compiler/Modules/YourModule.lean.
  2. Import Compiler.ECM and Compiler.CompilationModel.
  3. Define an ExternalCallModule structure with:
    • name: human-readable identifier for error messages
    • numArgs: expected argument count
    • resultVars: names of local variables this module binds (empty for fire-and-forget)
    • writesState / readsState: mutability flags (govern view/pure enforcement)
    • compile: function producing List YulStmt from compiled YulExpr arguments
    • axioms: trust assumptions this module introduces
  4. Add a convenience wrapper that returns Stmt.ecm yourModule args.
  5. Add compile-time tests in CompilationModelFeatureTest.lean.

Checklist

  • Module compiles (lake build Compiler.Modules.YourModule)
  • Convenience wrapper returns Stmt.ecm with correct argument list
  • writesState/readsState flags are accurate (tested via view/pure rejection)
  • axioms list documents all trust assumptions
  • Compile-time smoke test added to CompilationModelFeatureTest.lean
  • Any validation (selector bounds, parameter names) is in compile, not deferred

Standard vs. Third-Party

Standard modules live here and ship with Verity. They cover widely-used patterns (ERC-20 writes and reads, ERC-4626 preview calls, oracle reads, EVM precompiles, flash-loan callbacks, generic ABI calls).

Protocol-specific modules (Uniswap, Chainlink, Aave) should live in external Lean packages that depend on Compiler.ECM. See docs/EXTERNAL_CALL_MODULES.md for the full guide.