Add generic Solidity ergonomics to Verity macro

Compiler/CompilationModel/ValidationCalls.lean

@@ -126,6 +126,16 @@ def linkedExternalCallYulArgCountForParam : ParamType → Nat
 def linkedExternalCallYulArgCount (params : List ParamType) : Nat :=
   params.foldl (fun acc paramTy => acc + linkedExternalCallYulArgCountForParam paramTy) 0
 
+def linkedExternalReturnYulCountForType : ParamType → Nat
+  | ParamType.tuple elemTys =>
+      elemTys.foldl (fun acc elemTy => acc + linkedExternalReturnYulCountForType elemTy) 0
+  | ParamType.fixedArray elemTy size =>
+      size * linkedExternalReturnYulCountForType elemTy
+  | _ => 1
+
+def linkedExternalReturnYulCount (returns : List ParamType) : Nat :=
+  returns.foldl (fun acc retTy => acc + linkedExternalReturnYulCountForType retTy) 0
+
 def findInternalFunctionByName (functions : List FunctionSpec)
     (callerName calleeName : String) : Except String FunctionSpec := do
   let candidates := functions.filter (fun fn => fn.isInternal && fn.name == calleeName)
@@ -611,8 +621,9 @@ def validateExternalCallTargetsInStmt
           if args.length != expectedArgs then
             throw s!"Compilation error: {context} calls external function '{externalName}' with {args.length} Yul arg(s), expected {expectedArgs}."
           let returns ← externalFunctionReturns ext
-          if returns.length != resultVars.length then
-            throw s!"Compilation error: {context} binds {resultVars.length} values from external function '{externalName}', but it returns {returns.length}."
+          let expectedReturns := linkedExternalReturnYulCount returns
+          if expectedReturns != resultVars.length then
+            throw s!"Compilation error: {context} binds {resultVars.length} Yul value(s) from external function '{externalName}', but it returns {expectedReturns} Yul value(s)."
           let rec checkDuplicateVars (seen : List String) : List String → Except String Unit
             | [] => pure ()
             | name :: rest =>
@@ -631,8 +642,9 @@ def validateExternalCallTargetsInStmt
           if args.length != expectedArgs then
             throw s!"Compilation error: {context} calls external function '{externalName}' with {args.length} Yul arg(s), expected {expectedArgs}."
           let returns ← externalFunctionReturns ext
-          if returns.length != resultVars.length then
-            throw s!"Compilation error: {context} binds {resultVars.length} values from external function '{externalName}', but it returns {returns.length}."
+          let expectedReturns := linkedExternalReturnYulCount returns
+          if expectedReturns != resultVars.length then
+            throw s!"Compilation error: {context} binds {resultVars.length} Yul value(s) from external function '{externalName}', but it returns {expectedReturns} Yul value(s)."
           let tryName := s!"{externalName}_try"
           match externals.find? (fun candidate => candidate.name == tryName) with
           | none =>
@@ -641,9 +653,13 @@ def validateExternalCallTargetsInStmt
               if tryExt.params != ext.params then
                 throw s!"Compilation error: try wrapper '{tryName}' must take the same parameters as external function '{externalName}'."
               let tryReturns ← externalFunctionReturns tryExt
-              let expectedTryReturns := ParamType.bool :: returns
-              if tryReturns != expectedTryReturns then
-                throw s!"Compilation error: try wrapper '{tryName}' must return Bool followed by the return values of external function '{externalName}'."
+              let validTryReturns :=
+                match tryReturns with
+                | ParamType.bool :: tryTail =>
+                    linkedExternalReturnYulCount tryTail == linkedExternalReturnYulCount returns
+                | _ => false
+              if !validTryReturns then
+                throw s!"Compilation error: try wrapper '{tryName}' must return Bool followed by the flattened return values of external function '{externalName}'."
           let allVars := successVar :: resultVars
           let rec checkDuplicateTryVars (seen : List String) : List String → Except String Unit
             | [] => pure ()

Compiler/CompilationModelFeatureTest.lean

@@ -4314,7 +4314,7 @@ set_option maxRecDepth 4096 in
   expectCompileErrorContains
     "effect-only external call bind still rejects non-void externals"
     effectOnlyExternalBindMismatchSpec
-    "binds 0 values from external function 'echo', but it returns 1."
+    "binds 0 Yul value(s) from external function 'echo', but it returns 1 Yul value(s)."
   expectCompileErrorContains
     "reserved builtin exp name cannot be shadowed by externals"
     reservedBuiltinExpExternalSpec

Contracts/Common.lean

@@ -218,6 +218,7 @@ def arrayLength {α : Type} (values : Array α) : Uint256 := values.size
 def arrayElement {α : Type} [Inhabited α] (values : Array α) (index : Uint256) : α :=
   values.getD (index : Nat) (Inhabited.default : α)
 def abiHeadWord {α : Type} [Inhabited α] (_value : α) (_wordOffset : Uint256) : Uint256 := 0
+def abiEncode {α : Type} [Inhabited α] (_value : α) : Uint256 := 0
 def arrayElementChecked {α : Type} (values : Array α) (index : Uint256) : Contract α := fun state =>
   if h : (index : Nat) < values.size then
     ContractResult.success (values[(index : Nat)]'h) state
@@ -236,26 +237,31 @@ def returnBytes {α : Type} (value : α) : Contract α := pure value
 def returnStorageWords {α : Type} (_slots : Array α) : Contract (Array Uint256) := pure #[]
 
 inductive EventArg where
-  | word (value : Uint256)
-  | dynamicArray (length : Uint256)
-deriving Repr, DecidableEq
+  | word (value : Contract Uint256)
+  | dynamicArray (length : Contract Uint256)
 
 namespace EventArg
 
-def toWord : EventArg → Uint256
+def toWord : EventArg → Contract Uint256
   | .word value => value
   | .dynamicArray length => length
 
 end EventArg
 
 instance : Coe Uint256 EventArg where
-  coe value := EventArg.word value
+  coe value := EventArg.word (pure value)
 
 instance (α : Type) : CoeTC (Array α) EventArg where
-  coe values := EventArg.dynamicArray values.size
+  coe values := EventArg.dynamicArray (pure values.size)
 
-def emit (name : String) (args : List EventArg) : Contract Unit :=
-  emitEvent name (args.map EventArg.toWord)
+instance (α : Type) : CoeTC (Contract (Array α)) EventArg where
+  coe values := EventArg.dynamicArray (do
+    let array ← values
+    pure array.size)
+
+def emit (name : String) (args : List EventArg) : Contract Unit := do
+  let words ← args.mapM EventArg.toWord
+  emitEvent name words
 def setPackedStorage {α : Type} (rootSlot : StorageSlot α) (wordOffset : Nat)
     (word : Uint256) : Contract Unit := fun state =>
   let targetSlot := (rootSlot.slot + wordOffset) % Compiler.Constants.evmModulus

Contracts/Smoke.lean

@@ -1069,7 +1069,7 @@ verity_contract NamedStructStorageRejected where
     return 0
 
 /--
-error: non-leaf struct parameter projection is not supported; project a scalar or static single-word leaf field instead (#1832)
+error: unknown variable 'feeConfig.borrowTakerFeeRatio'
 -/
 #guard_msgs in
 verity_contract NamedStructNonLeafProjectionRejected where
@@ -1088,7 +1088,7 @@ verity_contract NamedStructNonLeafProjectionRejected where
     return feeConfig.borrowTakerFeeRatio
 
 /--
-error: non-leaf struct parameter projection is not supported; project a scalar or static single-word leaf field instead (#1832)
+error: unknown variable 'pair_0'
 -/
 #guard_msgs in
 verity_contract NamedStructTupleProjectionRejected where
@@ -1390,6 +1390,11 @@ example :
       , Compiler.CompilationModel.Stmt.stop
       ] := rfl
 
+example :
+    (emit "Batch" [(returnArray #[(1 : Uint256), 2, 3] : Contract (Array Uint256))]
+        |>.run Verity.defaultState).getState.events =
+      [{ name := "Batch", args := [3], indexedArgs := [] }] := rfl
+
 verity_contract ForEachMutableLocalSmoke where
   storage
     seen : Uint256 := slot 0
@@ -2019,7 +2024,7 @@ verity_contract ERC20HelperShadowWriteRejected where
     safeTransfer token toAddr amount
 
 /--
- error: linked external 'describe' uses unsupported return type; executable externalCall currently supports only Uint256, Int256, Uint8, Address, Bytes32, and Bool
+ error: linked external 'describe' uses unsupported return type; executable externalCall currently supports only word-like values and static ABI composites of word-like values
 -/
 #guard_msgs in
 verity_contract ExternalCallUnsupportedType where
@@ -2050,6 +2055,31 @@ verity_contract ExternalCallMultiReturn where
   function noop () : Unit := do
     pure ()
 
+verity_contract ExternalCallTupleReturn where
+  storage
+  linked_externals
+    external pair(Uint256) -> (Tuple [Uint256, Uint256])
+    external pair_try(Uint256) -> (Bool, Tuple [Uint256, Uint256])
+
+  function noop () : Unit := do
+    pure ()
+
+verity_contract ExternalCallTryWrapperMissingBoolRejected where
+  storage
+  linked_externals
+    external pair(Uint256) -> (Uint256, Uint256)
+    external pair_try(Uint256) -> (Uint256, Uint256, Uint256)
+
+  function badTry (x : Uint256) : Uint256 := do
+    let (_success, a, b) ← tryExternalCall "pair" [x]
+    return add a b
+
+/--
+error: #check_contract failed for 'Contracts.Smoke.ExternalCallTryWrapperMissingBoolRejected': Compilation error: try wrapper 'pair_try' must return Bool followed by the flattened return values of external function 'pair'.
+-/
+#guard_msgs in
+#check_contract ExternalCallTryWrapperMissingBoolRejected
+
 /--
 error: ecmDo requires an effect-only ECM module, but 'oracleReadUint256' binds 1 result value(s)
 -/

Verity/Macro/Elaborate.lean

@@ -13,13 +13,26 @@ set_option hygiene false
 
 @[command_elab verityContractCmd]
 def elabVerityContract : CommandElab := fun stx => do
-  let (contractName, _newtypeDecls, structDecls, adtDecls, fields, errorDecls, eventDecls, constDecls, immutableDecls, externalDecls, ctor, functions, storageNamespace) ← parseContractSyntax stx
+  let parsed ← parseContractSyntax stx
+  let contractName := parsed.contractName
+  let structDecls := parsed.structDecls
+  let adtDecls := parsed.adtDecls
+  let fields := parsed.fields
+  let errorDecls := parsed.errorDecls
+  let eventDecls := parsed.eventDecls
+  let constDecls := parsed.constDecls
+  let immutableDecls := parsed.immutableDecls
+  let externalDecls := parsed.externalDecls
+  let ctor := parsed.ctor
+  let modifiers := parsed.modifiers
+  let functions := parsed.functions
+  let storageNamespace := parsed.storageNamespace
 
   validateGeneratedDefNamesPublic fields constDecls immutableDecls functions
   validateConstantDeclsPublic constDecls
   validateImmutableDeclsPublic fields constDecls immutableDecls ctor
   validateExternalDeclsPublic externalDecls
-  validateFunctionDeclsPublic fields errorDecls constDecls immutableDecls externalDecls ctor functions
+  validateFunctionDeclsPublic fields errorDecls constDecls immutableDecls externalDecls ctor modifiers functions
 
   elabCommand (← `(namespace $contractName))
   try
@@ -49,7 +62,7 @@ def elabVerityContract : CommandElab := fun stx => do
         elabCommand cmd
       elabCommand (← mkBridgeCommand fn.ident)
 
-    elabCommand (← mkSpecCommandPublic (toString contractName.getId) fields errorDecls eventDecls constDecls immutableDecls externalDecls ctor functions adtDecls storageNamespace)
+    elabCommand (← mkSpecCommandPublic (toString contractName.getId) fields errorDecls eventDecls constDecls immutableDecls externalDecls ctor modifiers functions adtDecls storageNamespace)
 
     let findIdxSimpCmds ← mkFindIdxFieldSimpCommandsPublic contractName fields
     for cmd in findIdxSimpCmds do

Verity/Macro/Syntax.lean

@@ -26,6 +26,8 @@ declare_syntax_cat verityAdtVariant
 declare_syntax_cat verityAdtDecl
 declare_syntax_cat verityNamespaceSpec
 declare_syntax_cat veritySpecialEntrypoint
+declare_syntax_cat verityModifier
+declare_syntax_cat verityModifierUse
 declare_syntax_cat verityFunction
 
 syntax ident " : " term " := " "slot" num : verityStorageField
@@ -78,7 +80,9 @@ syntax "constructor " "(" sepBy(verityParam, ",") ")" (ppSpace verityLocalObliga
 syntax "constructor " "(" sepBy(verityParam, ",") ")" " payable" (ppSpace verityLocalObligations)? " := " term : verityConstructor
 syntax "receive" (ppSpace verityLocalObligations)? " := " term : veritySpecialEntrypoint
 syntax "fallback" (ppSpace verityLocalObligations)? " := " term : veritySpecialEntrypoint
-syntax "function " verityMutability* ident " (" sepBy(verityParam, ",") ")" (ppSpace verityInitGuard)? (ppSpace verityRequiresRole)? (ppSpace verityModifies)? (ppSpace verityLocalObligations)? " : " term " := " term : verityFunction
+syntax "modifier " ident " := " term : verityModifier
+syntax "with " sepBy1(ident, ",") : verityModifierUse
+syntax "function " verityMutability* ident " (" sepBy(verityParam, ",") ")" (ppSpace verityInitGuard)? (ppSpace verityModifierUse)? (ppSpace verityRequiresRole)? (ppSpace verityModifies)? (ppSpace verityLocalObligations)? " : " term " := " term : verityFunction
 
 syntax (name := verityContractCmd)
   "verity_contract " ident " where "
@@ -94,6 +98,7 @@ syntax (name := verityContractCmd)
   ("linked_externals " verityExternal+)?
   (verityConstructor)?
   (veritySpecialEntrypoint)*
+  (verityModifier)*
   verityFunction* : command
 
 syntax (name := checkContractCmd)