feat: first-class modifiers and single inheritance (#2087)

Contracts/Smoke/InheritanceImportBase.lean

@@ -0,0 +1,14 @@
+import Contracts.Common
+
+namespace Contracts.Smoke.InheritanceImport
+
+open Contracts
+open Verity hiding pure bind
+
+verity_contract ImportedInheritanceBase where
+  types
+    ImportedAmount : Uint256
+  storage
+    inheritedValue : Uint256 := slot 0
+
+end Contracts.Smoke.InheritanceImport

Contracts/Smoke/InheritanceImportChild.lean

@@ -0,0 +1,20 @@
+import Contracts.Smoke.InheritanceImportBase
+import Compiler.CheckContract
+
+namespace Contracts.Smoke.InheritanceImport
+
+open Contracts
+open Verity hiding pure bind
+
+-- The parent is loaded exclusively from InheritanceImportBase.olean. This
+-- fails if inheritance metadata is held in process-local state.
+verity_contract ImportedInheritanceChild is ImportedInheritanceBase where
+  storage
+    childValue : Uint256 := slot 1
+
+  function setImported (next : ImportedAmount) : Unit := do
+    setStorage inheritedValue next
+
+#check_contract ImportedInheritanceChild
+
+end Contracts.Smoke.InheritanceImport

Verity/Macro/Elaborate.lean

@@ -90,6 +90,7 @@ def elabVerityContract : CommandElab := fun stx => do
   validateExternalDeclsPublic externalDecls
   validateFunctionDeclsPublic fields errorDecls constDecls immutableDecls externalDecls ctor modifiers functions
 
+  let declarationNs ← getCurrNamespace
   elabCommand (← `(namespace $contractName))
   try
     for constant in constDecls do
@@ -149,6 +150,8 @@ def elabVerityContract : CommandElab := fun stx => do
       if fn.isPure then
         elabCommand (← mkPureTheoremCommand fn)
 
+    registerContractSyntax (declarationNs ++ contractName.getId) parsed
+
     -- Emit per-function _no_calls theorems for no_external_calls functions (#1729, Axis 3 Step 1c).
     for fn in functions do
       if fn.noExternalCalls then

Verity/Macro/Interfaces.lean

@@ -116,8 +116,6 @@ def parseInterface
   match stx with
   | `(verityInterface| interface $name:ident where $[$fns:verityInterfaceFunction]* end) =>
       let parsedFns ← fns.mapM (parseInterfaceFunction newtypes structDecls adtDecls)
-      if parsedFns.isEmpty then
-        throwErrorAt name s!"interface '{toString name.getId}' must declare at least one function"
       pure { ident := name, name := toString name.getId, functions := parsedFns }
   | _ => throwErrorAt stx "invalid interface declaration"
 

Verity/Macro/Syntax.lean

@@ -34,6 +34,7 @@ declare_syntax_cat verityNamespaceSpec
 declare_syntax_cat veritySpecialEntrypoint
 declare_syntax_cat verityModifier
 declare_syntax_cat verityModifierUse
+declare_syntax_cat verityDispatch
 declare_syntax_cat verityRoleDecl
 declare_syntax_cat verityFunction
 declare_syntax_cat verityIntrinsicClause
@@ -96,6 +97,8 @@ syntax "allow_post_interaction_writes" : verityMutability
 syntax "nonreentrant(" ident ")" : verityMutability
 syntax "cei_safe" : verityMutability
 syntax "reentrancy_trusted" : verityMutability
+syntax "virtual" : verityDispatch
+syntax "override" : verityDispatch
 syntax "modifies(" sepBy1(ident, ",") ")" : verityModifies
 syntax "requires(" ident ")" : verityRequiresRole
 syntax ident " : " term:max : verityNewtype
@@ -151,14 +154,14 @@ syntax "requireError " term:max ppSpace ident "(" sepBy(term, ",") ")" : doElem
 syntax (name := requireSomeUintErrorTerm) "requireSomeUintError " term:max ppSpace ident "(" sepBy(term, ",") ")" : term
 syntax "ecmBind " term:max ppSpace term:max ppSpace term:max : doElem
 syntax (priority := high) "unsafe " str " do " doSeq : doElem
-syntax "constructor " "(" sepBy(verityParam, ",") ")" (ppSpace verityLocalObligations)? " := " term : verityConstructor
-syntax "constructor " "(" sepBy(verityParam, ",") ")" " payable" (ppSpace verityLocalObligations)? " := " term : verityConstructor
+syntax "constructor " "(" sepBy(verityParam, ",") ")" (ppSpace ident "(" sepBy(term, ",") ")")? (ppSpace verityLocalObligations)? " := " term : verityConstructor
+syntax "constructor " "(" sepBy(verityParam, ",") ")" " payable" (ppSpace ident "(" sepBy(term, ",") ")")? (ppSpace verityLocalObligations)? " := " term : verityConstructor
 syntax "receive" (ppSpace verityLocalObligations)? " := " term : veritySpecialEntrypoint
 syntax "fallback" (ppSpace verityLocalObligations)? " := " term : veritySpecialEntrypoint
 syntax "modifier " ident " := " term : verityModifier
 syntax "with " sepBy1(ident, ",") : verityModifierUse
 syntax ident " := " ident : verityRoleDecl
-syntax "function " verityMutability* (pureMutabilityMarker)? verityMutability* ident " (" sepBy(verityParam, ",") ")" (ppSpace verityInitGuard)? (ppSpace verityModifierUse)? (ppSpace verityRequiresRole)? (ppSpace verityModifies)? (ppSpace verityLocalObligations)? " : " term " := " term : verityFunction
+syntax "function " verityMutability* (pureMutabilityMarker)? verityMutability* verityDispatch* ident " (" sepBy(verityParam, ",") ")" (ppSpace verityInitGuard)? (ppSpace verityModifierUse)? (ppSpace verityRequiresRole)? (ppSpace verityModifies)? (ppSpace verityLocalObligations)? " : " term " := " term : verityFunction
 
 -- verity_intrinsic syntax (minimal one-argument shape for consumer-owned intrinsics)
 -- `pure` is parsed as an identifier here to avoid reserving it as a global
@@ -190,7 +193,7 @@ syntax (name := verityIntrinsicCmd)
   ident " := " term ";" ident "[" sepBy(verityIntrinsicObligation, ",") "]" : command
 
 syntax (name := verityContractCmd)
-  "verity_contract " ident " where "
+  "verity_contract " ident (" is " ident)? " where "
   ("types " verityNewtype+)?
   ("inductive " verityAdtDecl+)?
   (verityNamespaceSpec)?