feat(edsl): add uint8-backed enum support

Compiler/ABI.lean

@@ -27,6 +27,7 @@ private def abiTypeString : ParamType → String
   | .array t => abiTypeString t ++ "[]"
   | .fixedArray t n => abiTypeString t ++ "[" ++ toString n ++ "]"
   | .adt _ _ => "tuple"  -- ADTs are ABI-encoded as static tuples
+  | .newtypeOf "__verity_enum" _ => "uint8"
   | .newtypeOf _ baseType => abiTypeString baseType  -- Erased to base type
 
 -- Uses `fieldTypeToParamType` from CompilationModel (shared, not duplicated).

Compiler/CompilationModel/AbiHelpers.lean

@@ -63,6 +63,7 @@ mutual
     | ParamType.adt _name maxFields =>
         -- ABI-encoded as static tuple: (uint8, uint256, ..., uint256)
         "(" ++ String.intercalate "," ("uint8" :: List.replicate maxFields "uint256") ++ ")"
+    | ParamType.newtypeOf "__verity_enum" _ => "uint8"
     | ParamType.newtypeOf _ baseType => paramTypeToSolidityString baseType  -- Erased to base type
 
   private def paramTypeListToSolidityStrings : List ParamType → List String

Contracts/Common.lean

@@ -168,7 +168,7 @@ macro_rules
           $(Lean.quote (toString errorName.getId))
           [ $[$encodedArgs],* ])
   | `(doElem| panic($code:term)) => do
-      let panicFn := Lean.mkIdentFrom code `_root_.Contracts.revertPanic
+      let panicFn := Lean.mkIdentFrom code `_root_.Contracts.revertPanicAs
       `(doElem| $panicFn:ident $code)
   | `(requireSomeUintError $optExpr:term $errorName:ident($args,*)) => do
       let requireFn := Lean.mkIdentFrom errorName `_root_.Contracts.requireSomeUintCustomError
@@ -317,6 +317,12 @@ decimal panic code; on-chain the compiled contract reverts with the ABI-encoded
 def revertPanic (code : Uint256) : Contract Unit :=
   revertCustomError "Panic" [CustomErrorArg.encode code]
 
+/-- Polymorphic executable counterpart used when a terminating panic appears in
+an expression-valued generated body. Keep `revertPanic`'s public signature
+source-compatible for direct callers. -/
+def revertPanicAs {α : Type} (code : Uint256) : Contract α :=
+  fun state => ContractResult.revert s!"Panic({code.val})" state
+
 private def wordToSigned (value : Uint256) : Int :=
   (toInt256 value : Int)
 

Contracts/Smoke/EnumFeatureTest.lean

@@ -0,0 +1,94 @@
+import Contracts.Common
+
+namespace Contracts.Smoke.EnumFeatureTest
+
+open Compiler.CompilationModel
+open Verity hiding pure bind
+open Verity.EVM.Uint256
+
+verity_contract MacroEnumUsage where
+  enums
+    enum Status { Pending, Active, Closed }
+
+  storage
+    status : Status := slot 0
+    statuses : Uint256 → Status := slot 1
+
+  errors
+    error InvalidStatus(Status)
+
+  event_defs
+    event StatusChanged(@indexed previous : Status, current : Status)
+
+  function identity (value : Status) : Status := do
+    return value
+
+  function active () : Status := do
+    return Status.Active
+
+  function castStatus (value : Uint256) : Status := do
+    let casted ← Status(value)
+    return casted
+
+  function setStatus (value : Status) : Unit := do
+    setStorage status value
+
+  function getStatus () : Status := do
+    let value ← getStorage status
+    return value
+
+  function setStatusAt (key : Uint256, value : Status) : Unit := do
+    setMappingUint statuses key value
+
+  function getStatusAt (key : Uint256) : Status := do
+    let value ← getMappingUint statuses key
+    return value
+
+def identityUsesUint8Abi : Bool :=
+  (match MacroEnumUsage.identity_model.params with
+   | [{ ty, .. }] => paramTypeToSolidityString ty == "uint8"
+   | _ => false) &&
+    MacroEnumUsage.identity_model.returns == [ParamType.uint8]
+
+example : identityUsesUint8Abi = true := by native_decide
+
+def eventAndErrorUseUint8Abi : Bool :=
+  MacroEnumUsage.spec.events.any (fun ev =>
+    match ev with
+    | { name := "StatusChanged", params :=
+        [{ name := "previous", ty := ParamType.uint8, kind := EventParamKind.indexed },
+         { name := "current", ty := ParamType.uint8, kind := EventParamKind.unindexed }] } => true
+    | _ => false) &&
+  MacroEnumUsage.spec.errors.any (fun err =>
+    match err with
+    | { name := "InvalidStatus", params := [ParamType.uint8] } => true
+    | _ => false)
+
+example : eventAndErrorUseUint8Abi = true := by native_decide
+
+def memberConstantIsOne : Bool := MacroEnumUsage.Status.Active == 1
+
+example : memberConstantIsOne = true := by native_decide
+
+def castAcceptsLastMember : Bool :=
+  match MacroEnumUsage.castStatus 2 defaultState with
+  | .success value _ => value == 2
+  | .revert _ _ => false
+
+example : castAcceptsLastMember = true := by native_decide
+
+def castRejectsOutOfRange : Bool :=
+  match MacroEnumUsage.castStatus 3 defaultState with
+  | .success _ _ => false
+  | .revert _ _ => true
+
+example : castRejectsOutOfRange = true := by native_decide
+
+def enumParamRejectsOutOfRange : Bool :=
+  match MacroEnumUsage.identity 3 defaultState with
+  | .success _ _ => false
+  | .revert _ _ => true
+
+example : enumParamRejectsOutOfRange = true := by native_decide
+
+end Contracts.Smoke.EnumFeatureTest

Verity/Macro/Bridge.lean

@@ -247,12 +247,14 @@ private def mkFieldFrameConjunct (field : StorageFieldDecl) : CommandElabM Term
   | .dynamicArray _ =>
       -- storageArray slot is unchanged
       `(s'.storageArray $slotLit = s.storageArray $slotLit)
-  | .mappingAddressToUint256 | .mappingStruct .address _ =>
+  | .mappingAddressToUint256 | .mappingAddressToEnum _ _ | .mappingStruct .address _ =>
       -- ∀ k, s'.storageMap slot k = s.storageMap slot k
       `(∀ k, s'.storageMap $slotLit k = s.storageMap $slotLit k)
-  | .mappingUintToUint256 | .mappingStruct .uint256 _ =>
+  | .mappingUintToUint256 | .mappingUintToEnum _ _ | .mappingStruct .uint256 _ =>
       `(∀ k, s'.storageMapUint $slotLit k = s.storageMapUint $slotLit k)
-  | .mappingStruct .bytes32 _ | .mappingChain _ | .mapping2AddressToAddressToUint256 | .mappingStruct2 _ _ _ =>
+  | .mappingStruct .bytes32 _ | .mappingChain _ | .mappingChainEnum _ _ _
+    | .mapping2AddressToAddressToUint256 | .mapping2AddressToAddressToEnum _ _
+    | .mappingStruct2 _ _ _ =>
       -- These shapes compile to hashed `storage` slots rather than the legacy
       -- storageMap mirrors, so the conservative frame predicate must constrain
       -- the hashed storage surface.

Verity/Macro/ExternalCalls.lean

@@ -59,6 +59,7 @@ def parseExternal
 private def externalExecutableWordType? : ValueType → Bool
   | .uint256 | .int256 | .uint8 | .uint16 | .uintN _ | .intN _ | .bytesN _
   | .address | .bytes32 | .bool => true
+  | .enum _ _ => true
   | .newtype _ baseType => externalExecutableWordType? baseType
   | _ => false
 

Verity/Macro/Functions.lean

@@ -24,6 +24,7 @@ partial def valueTypeSignatureComponent : ValueType → String
   | .fixedArray ty size => "fixed_array_" ++ toString size ++ "_" ++ valueTypeSignatureComponent ty
   | .tuple tys => "tuple" ++ toString tys.length ++ "_" ++ String.intercalate "__" (tys.map valueTypeSignatureComponent)
   | .newtype name baseType => "newtype_" ++ name ++ "_" ++ valueTypeSignatureComponent baseType
+  | .enum name _ => "enum_" ++ name
   | .struct name fields =>
       "struct_" ++ name ++ "_" ++
         String.intercalate "__" (fields.map (fun field => field.fst ++ "_" ++ valueTypeSignatureComponent field.snd))
@@ -34,6 +35,7 @@ def functionSignatureKey (fn : FunctionDecl) : String :=
 
 partial def valueTypeAbiSignatureComponent : ValueType → String
   | .newtype _ baseType => valueTypeAbiSignatureComponent baseType
+  | .enum _ _ => "scalar_uint8"
   | .array ty => "array_" ++ valueTypeAbiSignatureComponent ty
   | .fixedArray ty size => "fixed_array_" ++ toString size ++ "_" ++ valueTypeAbiSignatureComponent ty
   | .tuple tys => "tuple" ++ toString tys.length ++ "_" ++ String.intercalate "__" (tys.map valueTypeAbiSignatureComponent)

Verity/Macro/Interfaces.lean

@@ -27,6 +27,7 @@ partial def valueTypeToSolidityString : ValueType → String
   | .struct _ fields =>
       "(" ++ String.intercalate "," (fields.map (fun field => valueTypeToSolidityString field.snd)) ++ ")"
   | .newtype _ baseType => valueTypeToSolidityString baseType
+  | .enum _ _ => "uint8"
   | .adt name _ => name
   | .unit => "()"
 

Verity/Macro/Internal.lean

@@ -1,6 +1,7 @@
 import Lean
 import Compiler.CompilationModel.InternalNaming
 import Verity.Macro.Types
+import Verity.Macro.Syntax
 
 namespace Verity.Macro
 
@@ -10,7 +11,10 @@ open Lean.Elab.Command
 def localFunctionAppSyntax?
     (stx : Term) : Option (String × Array Term) :=
   let stx := stripParens stx
-  match stx.raw with
+  match stx with
+  | `(term| $fn:ident($[$args:term],*)) =>
+      some (toString fn.getId, args)
+  | _ => match stx.raw with
   | .node _ `Lean.Parser.Term.app args =>
       match args.getD 0 Syntax.missing with
       | .ident _ raw _ _ =>

Verity/Macro/Storage.lean

@@ -52,6 +52,7 @@ def storageTypeFromSyntax
   let rec storageStructMemberElementWords (memberName : String) : ValueType → CommandElabM Nat
     | .uint256 | .int256 | .uint16 | .address | .bool | .bytes32 => pure 1
     | .newtype _ baseType => storageStructMemberElementWords memberName baseType
+    | .enum _ _ => pure 1
     | .fixedArray elemTy size => do
         let elemWords ← storageStructMemberElementWords memberName elemTy
         pure (elemWords * size)
@@ -64,6 +65,8 @@ def storageTypeFromSyntax
     match memberTy with
     | .newtype _ baseType =>
         expandStructMemberDecl memberPrefix baseOffset baseType packed
+    | .enum _ _ =>
+        pure [{ name := memberPrefix, ty := memberTy, wordOffset := baseOffset, packed := packed }]
     | .fixedArray elemTy size => do
         if packed.isSome then
           throwErrorAt ty s!"mapping struct fixed-array member '{memberPrefix}' cannot be packed"
@@ -94,16 +97,23 @@ def storageTypeFromSyntax
 
   let (arrowArgs, arrowResult) ← collectArrowChainTypes ty
   if !arrowArgs.isEmpty then
-    match arrowResult with
-    | `(term| Uint256) =>
+    match (← valueTypeFromSyntax newtypes structDecls adtDecls arrowResult) with
+    | .uint256 =>
         let keyTypes ← arrowArgs.mapM keyTypeFromSyntax
         match keyTypes with
         | [.address] => pure .mappingAddressToUint256
         | [.uint256] => pure .mappingUintToUint256
         | [.address, .address] => pure .mapping2AddressToAddressToUint256
         | _ => pure (.mappingChain keyTypes)
+    | .enum name memberCount =>
+        let keyTypes ← arrowArgs.mapM keyTypeFromSyntax
+        match keyTypes with
+        | [.address] => pure (.mappingAddressToEnum name memberCount)
+        | [.uint256] => pure (.mappingUintToEnum name memberCount)
+        | [.address, .address] => pure (.mapping2AddressToAddressToEnum name memberCount)
+        | _ => pure (.mappingChainEnum keyTypes name memberCount)
     | _ =>
-        throwErrorAt ty "unsupported mapping value type; expected Uint256"
+        throwErrorAt ty "unsupported mapping value type; expected Uint256 or an enum"
   else
     match ty with
   | `(term| MappingStruct($keyTy:term,[ $[$members:verityStructMember],* ])) =>
@@ -132,14 +142,24 @@ def modelMappingKeyTypeTerm : MappingKeyType → CommandElabM Term
 
 def storageTypeMappingKeyTypes? : StorageType → Option (List MappingKeyType)
   | .mappingAddressToUint256 => some [.address]
+  | .mappingAddressToEnum _ _ => some [.address]
   | .mapping2AddressToAddressToUint256 => some [.address, .address]
+  | .mapping2AddressToAddressToEnum _ _ => some [.address, .address]
   | .mappingUintToUint256 => some [.uint256]
+  | .mappingUintToEnum _ _ => some [.uint256]
   | .mappingChain keyTypes => some keyTypes
+  | .mappingChainEnum keyTypes _ _ => some keyTypes
   | _ => none
 
 def storageTypeMappingDepth? (ty : StorageType) : Option Nat :=
   storageTypeMappingKeyTypes? ty |>.map List.length
 
+def storageTypeMappingValueType? : StorageType → Option ValueType
+  | .mappingAddressToEnum name memberCount | .mapping2AddressToAddressToEnum name memberCount
+    | .mappingUintToEnum name memberCount | .mappingChainEnum _ name memberCount =>
+      some (.enum name memberCount)
+  | _ => none
+
 def storageKeyTypeContractTerm : MappingKeyType → CommandElabM Term
   | .address => `(Address)
   | .uint256 => `(Uint256)
@@ -153,7 +173,7 @@ def modelStructMemberTerm (member : StructMemberDecl) : CommandElabM Term := do
         `(some { offset := $(natTerm offset), width := $(natTerm width) })
   let memberTypeTerm ←
     match member.ty with
-    | .uint256 | .int256 | .uint8 =>
+    | .uint256 | .int256 | .uint8 | .enum _ _ =>
         `(Compiler.CompilationModel.StructMemberType.uint256)
     | .uint16 =>
         `(Compiler.CompilationModel.StructMemberType.uint16)
@@ -193,6 +213,7 @@ def modelFieldTypeTerm (ty : StorageType) : CommandElabM Term :=
         "top-level named struct storage fields are not supported yet (#1758); flatten the struct into explicit scalar storage fields with fixed slots, or use MappingStruct/MappingStruct2 for struct-valued mappings"
   | .scalar .unit => throwError "storage fields cannot be Unit"
   | .scalar (.newtype _ baseType) => modelFieldTypeTerm (.scalar baseType)  -- Erased to base type
+  | .scalar (.enum _ _) => `(Compiler.CompilationModel.FieldType.uint256)
   | .scalar (.adt name maxFields) =>
       `(Compiler.CompilationModel.FieldType.adt $(Lean.quote name) $(Lean.quote maxFields))
   | .dynamicArray .uint256 => `(Compiler.CompilationModel.FieldType.dynamicArray Compiler.CompilationModel.StorageArrayElemType.uint256)
@@ -203,18 +224,33 @@ def modelFieldTypeTerm (ty : StorageType) : CommandElabM Term :=
   | .mappingAddressToUint256 =>
       `(Compiler.CompilationModel.FieldType.mappingTyped
           (Compiler.CompilationModel.MappingType.simple Compiler.CompilationModel.MappingKeyType.address))
+  | .mappingAddressToEnum _ _ =>
+      `(Compiler.CompilationModel.FieldType.mappingTyped
+          (Compiler.CompilationModel.MappingType.simple Compiler.CompilationModel.MappingKeyType.address))
   | .mapping2AddressToAddressToUint256 =>
       `(Compiler.CompilationModel.FieldType.mappingTyped
           (Compiler.CompilationModel.MappingType.nested
             Compiler.CompilationModel.MappingKeyType.address
             Compiler.CompilationModel.MappingKeyType.address))
+  | .mapping2AddressToAddressToEnum _ _ =>
+      `(Compiler.CompilationModel.FieldType.mappingTyped
+          (Compiler.CompilationModel.MappingType.nested
+            Compiler.CompilationModel.MappingKeyType.address
+            Compiler.CompilationModel.MappingKeyType.address))
   | .mappingUintToUint256 =>
       `(Compiler.CompilationModel.FieldType.mappingTyped
           (Compiler.CompilationModel.MappingType.simple Compiler.CompilationModel.MappingKeyType.uint256))
+  | .mappingUintToEnum _ _ =>
+      `(Compiler.CompilationModel.FieldType.mappingTyped
+          (Compiler.CompilationModel.MappingType.simple Compiler.CompilationModel.MappingKeyType.uint256))
   | .mappingChain keyTypes => do
       let keyTypeTerms := (← keyTypes.mapM modelMappingKeyTypeTerm).toArray
       `(Compiler.CompilationModel.FieldType.mappingTyped
           (Compiler.CompilationModel.MappingType.chain [ $[$keyTypeTerms],* ]))
+  | .mappingChainEnum keyTypes _ _ => do
+      let keyTypeTerms := (← keyTypes.mapM modelMappingKeyTypeTerm).toArray
+      `(Compiler.CompilationModel.FieldType.mappingTyped
+          (Compiler.CompilationModel.MappingType.chain [ $[$keyTypeTerms],* ]))
   | .mappingStruct keyType members => do
       let keyTypeTerm ← modelMappingKeyTypeTerm keyType
       let memberTerms := (← members.mapM modelStructMemberTerm).toArray

Verity/Macro/Syntax.lean

@@ -4,6 +4,10 @@ namespace Verity.Macro
 
 open Lean
 
+syntax:max ident noWs "(" sepBy(term, ",") ")" : term
+macro_rules
+  | `($fn:ident($[$args:term],*)) => `($fn $args*)
+
 declare_syntax_cat verityStorageField
 declare_syntax_cat verityStorageItem
 declare_syntax_cat verityStorageStructMember
@@ -27,6 +31,7 @@ declare_syntax_cat verityInitGuard
 declare_syntax_cat verityModifies
 declare_syntax_cat verityRequiresRole
 declare_syntax_cat verityNewtype
+declare_syntax_cat verityEnumDecl
 declare_syntax_cat verityStructDecl
 declare_syntax_cat verityAdtVariant
 declare_syntax_cat verityAdtDecl
@@ -99,6 +104,7 @@ syntax "reentrancy_trusted" : verityMutability
 syntax "modifies(" sepBy1(ident, ",") ")" : verityModifies
 syntax "requires(" ident ")" : verityRequiresRole
 syntax ident " : " term:max : verityNewtype
+syntax "enum " ident " {" sepBy1(ident, ",") "}" : verityEnumDecl
 syntax "struct " ident " where " sepBy1(verityParam, ",") : verityStructDecl
 syntax "| " ident "(" sepBy(verityParam, ",") ")" : verityAdtVariant
 syntax "| " ident : verityAdtVariant
@@ -192,6 +198,7 @@ syntax (name := verityIntrinsicCmd)
 syntax (name := verityContractCmd)
   "verity_contract " ident " where "
   ("types " verityNewtype+)?
+  ("enums " verityEnumDecl+)?
   ("inductive " verityAdtDecl+)?
   (verityNamespaceSpec)?
   "storage " verityStorageItem*