Add internal helpers and typed interface calls (#1949)

* Add internal helpers and typed interface calls

* Handle multi-argument typed interface calls

* Reject interface type name collisions

Author: Th0rgal

Contracts/Smoke.lean

@@ -16,6 +16,7 @@ import Compiler.Modules.Create2SSTORE2
 import Compiler.Modules.ERC20
 import Compiler.Modules.Oracle
 import Compiler.Modules.Precompiles
+import Contracts.Smoke.InternalInterfaceSmoke
 
 namespace Contracts.Smoke
 

Contracts/Smoke/InternalInterfaceSmoke.lean

@@ -0,0 +1,116 @@
+import Contracts.Common
+
+set_option linter.unusedVariables false
+
+namespace Contracts.Smoke
+
+open Verity hiding pure bind
+open Verity.EVM.Uint256
+
+verity_contract InternalHelperSmoke where
+  storage
+
+  function internal bump (x : Uint256) : Uint256 := do
+    return (add x 1)
+
+example :
+    (InternalHelperSmoke.spec.functions).any (fun fn =>
+      fn.name == "bump" && !fn.isInternal) = false := by
+  decide
+
+example :
+    (InternalHelperSmoke.spec.functions).any (fun fn =>
+      fn.name == "internal_bump" && fn.isInternal) = true := by
+  decide
+
+verity_contract TypedInterfaceCallSmoke where
+  storage
+
+  interfaces
+    interface IERC20 where
+      function balanceOf(Address) view returns (Uint256)
+      function transfer(Address, Uint256) returns (Bool)
+    end
+
+  function readBalance (token : IERC20, owner : Address) : Uint256 := do
+    let bal ← token.balanceOf owner
+    return bal
+
+  function readBalanceViaAlias (token : IERC20, owner : Address) : Uint256 := do
+    let t := token
+    let bal ← t.balanceOf owner
+    return bal
+
+  function transferToken (token : IERC20, recipient : Address, amount : Uint256) : Bool := do
+    let ok ← token.transfer recipient amount
+    return ok
+
+example :
+    (TypedInterfaceCallSmoke.spec.externals).any (fun ext =>
+      ext.name == "IERC20.balanceOf") = true := by
+  decide
+
+example :
+    (TypedInterfaceCallSmoke.spec.functions).any (fun fn =>
+      fn.name == "readBalance" &&
+        fn.body.any (fun stmt =>
+          match stmt with
+          | Compiler.CompilationModel.Stmt.ecm mod args =>
+              mod.name == "externalCallWithReturn" &&
+                mod.numArgs == 2 &&
+                mod.resultVars == ["bal"] &&
+                mod.readsState &&
+                !mod.writesState &&
+                args.length == 2
+          | _ => false)) = true := by
+  decide
+
+example :
+    (TypedInterfaceCallSmoke.spec.functions).any (fun fn =>
+      fn.name == "readBalanceViaAlias" &&
+        fn.body.any (fun stmt =>
+          match stmt with
+          | Compiler.CompilationModel.Stmt.ecm mod args =>
+              mod.name == "externalCallWithReturn" &&
+                mod.numArgs == 2 &&
+                mod.resultVars == ["bal"] &&
+                mod.readsState &&
+                !mod.writesState &&
+                args.length == 2
+          | _ => false)) = true := by
+  decide
+
+example :
+    (TypedInterfaceCallSmoke.spec.functions).any (fun fn =>
+      fn.name == "transferToken" &&
+        fn.body.any (fun stmt =>
+          match stmt with
+          | Compiler.CompilationModel.Stmt.ecm mod args =>
+                mod.name == "externalCallWithReturn" &&
+                mod.numArgs == 3 &&
+                mod.resultVars == ["ok"] &&
+                mod.readsState &&
+                mod.writesState &&
+                args.length == 3
+          | _ => false)) = true := by
+  decide
+
+/--
+error: interface name 'Clash' conflicts with an existing type name
+-/
+#guard_msgs in
+verity_contract InterfaceTypeNameClashRejected where
+  types
+    Clash : Uint256
+
+  storage
+
+  interfaces
+    interface Clash where
+      function read() view returns (Uint256)
+    end
+
+  function noop (_item : Clash) : Unit := do
+    pure ()
+
+end Contracts.Smoke

Verity/Macro/Syntax.lean

@@ -16,6 +16,9 @@ declare_syntax_cat verityConstant
 declare_syntax_cat verityImmutable
 declare_syntax_cat verityExternal
 declare_syntax_cat verityExternalLinkMode
+declare_syntax_cat verityInterface
+declare_syntax_cat verityInterfaceFunction
+declare_syntax_cat verityInterfaceParam
 declare_syntax_cat verityLocalObligation
 declare_syntax_cat verityLocalObligations
 declare_syntax_cat verityConstructor
@@ -67,10 +70,17 @@ syntax "external " ident "(" sepBy(term, ",") ")" : verityExternal
 syntax "external " ident "(" sepBy(term, ",") ")" " -> " "(" sepBy(term, ",") ")" : verityExternal
 syntax "external " ident "(" sepBy(term, ",") ")" ppSpace "linked_as" " := " verityExternalLinkMode : verityExternal
 syntax "external " ident "(" sepBy(term, ",") ")" " -> " "(" sepBy(term, ",") ")" ppSpace "linked_as" " := " verityExternalLinkMode : verityExternal
+syntax ident " : " term : verityInterfaceParam
+syntax "function " ident "(" sepBy(term, ",") ")" verityMutability* ident "(" sepBy(term, ",") ")" : verityInterfaceFunction
+syntax "function " ident " (" sepBy(term, ",") ")" verityMutability* ident "(" sepBy(term, ",") ")" : verityInterfaceFunction
+syntax "function " ident "(" sepBy(verityInterfaceParam, ",") ")" verityMutability* ident "(" sepBy(term, ",") ")" : verityInterfaceFunction
+syntax "function " ident " (" sepBy(verityInterfaceParam, ",") ")" verityMutability* ident "(" sepBy(term, ",") ")" : verityInterfaceFunction
+syntax "interface " ident " where " verityInterfaceFunction* "end" : verityInterface
 syntax ident " := " ident ppSpace str : verityLocalObligation
 syntax "local_obligations " "[" sepBy(verityLocalObligation, ",") "]" : verityLocalObligations
 syntax "payable" : verityMutability
 syntax "view" : verityMutability
+syntax "internal" : verityMutability
 syntax pureMutabilityMarker := &"pure"
 syntax "no_external_calls" : verityMutability
 syntax "allow_post_interaction_writes" : verityMutability
@@ -158,6 +168,7 @@ syntax (name := verityContractCmd)
   ("event_defs " verityEvent+)?
   ("constants " verityConstant+)?
   ("immutables " verityImmutable+)?
+  ("interfaces " verityInterface+)?
   ("linked_externals " verityExternal+)?
   (verityConstructor)?
   (veritySpecialEntrypoint)*