[Compiler Enhancement] Infer mutability through internal calls

Compiler/CompilationModel/Dispatch.lean

@@ -330,6 +330,9 @@ private def validateCompileInputsBeforeFieldWriteConflict
       throw s!"Compilation error: internal function name '{fn.name}' collides with an external function name in {spec.name}; internal function Yul definitions are keyed by name"
   | none =>
       pure ()
+  let functionEffects := inferFunctionEffects spec.functions
+  for fn in spec.functions do
+    validateFunctionSpecMutability functionEffects fn
   match firstDuplicateName (spec.errors.map (·.name)) with
   | some dup =>
       throw s!"Compilation error: duplicate custom error declaration '{dup}'"

Compiler/CompilationModelFeatureTest.lean

@@ -2968,6 +2968,86 @@ private def ceiInitialInternalCallAllowedSpec : CompilationModel := {
   ]
 }
 
+private def viewInternalReadInferenceSpec : CompilationModel := {
+  name := "ViewInternalReadInference"
+  fields := [{ name := "value", ty := FieldType.uint256 }]
+  «constructor» := none
+  functions := [
+    { name := "helper"
+      params := []
+      returnType := some FieldType.uint256
+      isInternal := true
+      body := [Stmt.return (Expr.storage "value")]
+    },
+    { name := "peek"
+      params := []
+      returnType := some FieldType.uint256
+      isView := true
+      body := [Stmt.return (Expr.internalCall "helper" [])]
+    }
+  ]
+}
+
+private def viewInternalWriteRejectedSpec : CompilationModel := {
+  name := "ViewInternalWriteRejected"
+  fields := [{ name := "value", ty := FieldType.uint256 }]
+  «constructor» := none
+  functions := [
+    { name := "helper"
+      params := []
+      returnType := none
+      isInternal := true
+      body := [Stmt.setStorage "value" (Expr.literal 1), Stmt.stop]
+    },
+    { name := "peek"
+      params := []
+      returnType := none
+      isView := true
+      body := [Stmt.internalCall "helper" [], Stmt.stop]
+    }
+  ]
+}
+
+private def pureInternalCallInferenceSpec : CompilationModel := {
+  name := "PureInternalCallInference"
+  fields := []
+  «constructor» := none
+  functions := [
+    { name := "helper"
+      params := [{ name := "value", ty := ParamType.uint256 }]
+      returnType := some FieldType.uint256
+      isInternal := true
+      body := [Stmt.return (Expr.add (Expr.param "value") (Expr.literal 1))]
+    },
+    { name := "next"
+      params := [{ name := "value", ty := ParamType.uint256 }]
+      returnType := some FieldType.uint256
+      isPure := true
+      body := [Stmt.return (Expr.internalCall "helper" [Expr.param "value"])]
+    }
+  ]
+}
+
+private def pureInternalReadRejectedSpec : CompilationModel := {
+  name := "PureInternalReadRejected"
+  fields := [{ name := "value", ty := FieldType.uint256 }]
+  «constructor» := none
+  functions := [
+    { name := "helper"
+      params := []
+      returnType := some FieldType.uint256
+      isInternal := true
+      body := [Stmt.return (Expr.storage "value")]
+    },
+    { name := "peek"
+      params := []
+      returnType := some FieldType.uint256
+      isPure := true
+      body := [Stmt.return (Expr.internalCall "helper" [])]
+    }
+  ]
+}
+
 private def ceiEcmWriteAfterCallRejectedSpec : CompilationModel := {
   name := "CEIEcmWriteAfterCallRejected"
   fields := [{ name := "value", ty := FieldType.uint256 }]
@@ -4499,6 +4579,12 @@ set_option maxRecDepth 4096 in
   expectTrue "macro payable constructor ABI reports payable state mutability"
     (contains payableCtorAbi "\"type\": \"constructor\"" &&
       contains payableCtorAbi "\"stateMutability\": \"payable\"")
+  expectTrue "macro pure function preserves model pure flag"
+    Contracts.Smoke.MutabilitySmoke.double_model.isPure
+  let mutabilityAbi := Compiler.ABI.emitContractABIJson Contracts.Smoke.MutabilitySmoke.spec
+  expectTrue "macro pure function ABI reports pure state mutability"
+    (contains mutabilityAbi "\"name\": \"double\"" &&
+      contains mutabilityAbi "\"stateMutability\": \"pure\"")
   let payableCtorContract ← expectCompile
     "macro payable constructor compiles"
     MacroPayableConstructorSmoke.MacroPayableConstructor.spec
@@ -4692,6 +4778,28 @@ set_option maxRecDepth 4096 in
     | .error _ => false
   expectTrue "CEI allows an initial internal-call statement without a prior interaction"
     ceiInitialInternalCallCompiled
+  let viewInternalReadInferenceCompiled :=
+    match Compiler.CompilationModel.compile viewInternalReadInferenceSpec
+        (selectorsFor viewInternalReadInferenceSpec) with
+    | .ok _ => true
+    | .error _ => false
+  expectTrue "view mutability accepts internal helpers inferred to only read state"
+    viewInternalReadInferenceCompiled
+  expectCompileErrorContains
+    "view mutability rejects internal helpers inferred to write state"
+    viewInternalWriteRejectedSpec
+    "function 'peek' is marked view but writes state"
+  let pureInternalCallInferenceCompiled :=
+    match Compiler.CompilationModel.compile pureInternalCallInferenceSpec
+        (selectorsFor pureInternalCallInferenceSpec) with
+    | .ok _ => true
+    | .error _ => false
+  expectTrue "pure mutability accepts internal helpers inferred to be pure"
+    pureInternalCallInferenceCompiled
+  expectCompileErrorContains
+    "pure mutability rejects internal helpers inferred to read state"
+    pureInternalReadRejectedSpec
+    "function 'peek' is marked pure but reads state/environment"
   expectCompileErrorContains
     "CEI rejects writing ECMs after an external call"
     ceiEcmWriteAfterCallRejectedSpec

Contracts/Smoke.lean

@@ -609,6 +609,9 @@ verity_contract MutabilitySmoke where
     let ownerAddr ← getStorageAddr owner
     return ownerAddr
 
+  function pure double (value : Uint256) : Uint256 := do
+    return (add value value)
+
 verity_contract SpecialEntrypointSmoke where
   storage
     receiveCount : Uint256 := slot 0

Verity/Macro/Bridge.lean

@@ -49,12 +49,26 @@ def mkViewTheoremCommand (fnDecl : FunctionDecl) : CommandElabM Cmd := do
   let modelName ← mkSuffixedIdent fnDecl.ident "_model"
   `(command|
     /-- Auto-generated: this function is declared `view` and its model
-        records that intent. The corresponding `stmtWritesState` validation
-        guarantees the body contains no state-writing statements. -/
+        records that intent. Function-effect validation guarantees the body and
+        any internal callees do not write state. -/
     @[simp] theorem $viewName :
         (Compiler.CompilationModel.FunctionSpec.isView
           ($modelName : Compiler.CompilationModel.FunctionSpec)) = true := rfl)
 
+/-- Auto-generated `_is_pure` theorem for pure functions.
+    Emits a `@[simp]` lemma stating the model's `isPure` flag is `true`, making this
+    fact available to downstream proof automation. Only called when `fnDecl.isPure`. -/
+def mkPureTheoremCommand (fnDecl : FunctionDecl) : CommandElabM Cmd := do
+  let pureName ← mkSuffixedIdent fnDecl.ident "_is_pure"
+  let modelName ← mkSuffixedIdent fnDecl.ident "_model"
+  `(command|
+    /-- Auto-generated: this function is declared `pure` and its model
+        records that intent. Function-effect validation guarantees the body and
+        any internal callees do not read or write state/environment. -/
+    @[simp] theorem $pureName :
+        (Compiler.CompilationModel.FunctionSpec.isPure
+          ($modelName : Compiler.CompilationModel.FunctionSpec)) = true := rfl)
+
 /-- Auto-generated `_no_calls` theorem for functions with a `no_external_calls` annotation
     (#1729, Axis 3 Step 1c).  Emits a `@[simp]` lemma stating the model's
     `noExternalCalls` flag is `true`.  Only called when `fnDecl.noExternalCalls`. -/
@@ -192,13 +206,14 @@ def mkFrameDefCommand
 /-- Count how many effect annotations are active on a function declaration. -/
 def effectAnnotationCount (fnDecl : FunctionDecl) : Nat :=
   (if fnDecl.isView then 1 else 0) +
+  (if fnDecl.isPure then 1 else 0) +
   (if fnDecl.noExternalCalls then 1 else 0) +
   (if !fnDecl.modifies.isEmpty then 1 else 0)
 
 /-- Auto-generated `_effects` conjunction theorem for functions with multiple
     effect annotations (#1729, Axis 3 Step 1d).  Bundles all individual effect
-    theorems (`_is_view`, `_no_calls`, `_modifies`) into a single `And` fact so
-    downstream proofs can obtain all guarantees in one `exact`. -/
+    theorems (`_is_view`, `_is_pure`, `_no_calls`, `_modifies`) into a single
+    `And` fact so downstream proofs can obtain all guarantees in one `exact`. -/
 def mkEffectsTheoremCommand (fnDecl : FunctionDecl) : CommandElabM Cmd := do
   let effectsName ← mkSuffixedIdent fnDecl.ident "_effects"
   let modelName ← mkSuffixedIdent fnDecl.ident "_model"
@@ -211,6 +226,12 @@ def mkEffectsTheoremCommand (fnDecl : FunctionDecl) : CommandElabM Cmd := do
         (Compiler.CompilationModel.FunctionSpec.isView
           ($modelName : Compiler.CompilationModel.FunctionSpec)) = true))
     proofs := proofs.push (← `($viewName))
+  if fnDecl.isPure then
+    let pureName ← mkSuffixedIdent fnDecl.ident "_is_pure"
+    conjuncts := conjuncts.push (← `(
+        (Compiler.CompilationModel.FunctionSpec.isPure
+          ($modelName : Compiler.CompilationModel.FunctionSpec)) = true))
+    proofs := proofs.push (← `($pureName))
   if fnDecl.noExternalCalls then
     let noCallsName ← mkSuffixedIdent fnDecl.ident "_no_calls"
     conjuncts := conjuncts.push (← `(

Verity/Macro/Elaborate.lean

@@ -87,6 +87,11 @@ def elabVerityContract : CommandElab := fun stx => do
       if fn.isView then
         elabCommand (← mkViewTheoremCommand fn)
 
+    -- Emit per-function _is_pure theorems for pure functions.
+    for fn in functions do
+      if fn.isPure then
+        elabCommand (← mkPureTheoremCommand fn)
+
     -- 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/Syntax.lean

@@ -66,6 +66,7 @@ syntax ident " := " ident ppSpace str : verityLocalObligation
 syntax "local_obligations " "[" sepBy(verityLocalObligation, ",") "]" : verityLocalObligations
 syntax "payable" : verityMutability
 syntax "view" : verityMutability
+syntax pureMutabilityMarker := &"pure"
 syntax "no_external_calls" : verityMutability
 syntax "allow_post_interaction_writes" : verityMutability
 syntax "nonreentrant(" ident ")" : verityMutability
@@ -102,7 +103,7 @@ syntax "receive" (ppSpace verityLocalObligations)? " := " term : veritySpecialEn
 syntax "fallback" (ppSpace verityLocalObligations)? " := " term : veritySpecialEntrypoint
 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 "function " verityMutability* (pureMutabilityMarker)? verityMutability* ident " (" sepBy(verityParam, ",") ")" (ppSpace verityInitGuard)? (ppSpace verityModifierUse)? (ppSpace verityRequiresRole)? (ppSpace verityModifies)? (ppSpace verityLocalObligations)? " : " term " := " term : verityFunction
 
 syntax (name := verityContractCmd)
   "verity_contract " ident " where "

Verity/Macro/Translate.lean

@@ -168,6 +168,7 @@ structure FunctionDecl where
   returnTy : ValueType
   isPayable : Bool := false
   isView : Bool := false
+  isPure : Bool := false
   noExternalCalls : Bool := false
   /-- When true, the function is annotated `allow_post_interaction_writes` and
       CEI (Checks-Effects-Interactions) enforcement is bypassed.  This is the
@@ -1029,6 +1030,7 @@ private def parseLocalObligation (stx : Syntax) : CommandElabM LocalObligationDe
 private structure ParsedMutability where
   isPayable : Bool := false
   isView : Bool := false
+  isPure : Bool := false
   noExternalCalls : Bool := false
   allowPostInteractionWrites : Bool := false
   nonReentrantLock : Option Ident := none
@@ -1149,8 +1151,9 @@ private def parseModifierUse (stx : TSyntax `verityModifierUse) : CommandElabM (
 
 private def parseFunction (newtypes : Array NewtypeDecl) (structDecls : Array StructDecl := #[]) (adtDecls : Array AdtDecl := #[]) (stx : Syntax) : CommandElabM FunctionDecl := do
   match stx with
-  | `(verityFunction| function $[$mods:verityMutability]* $name:ident ($[$params:verityParam],*) $[$guard?:verityInitGuard]? $[$modifierUse?:verityModifierUse]? $[$requiresRoleClause?:verityRequiresRole]? $[$modifiesClause?:verityModifies]? $[$localObligations?:verityLocalObligations]? : $retTy:term := $body:term) => do
-      let mut_ ← parseMutabilityModifiers mods stx
+  | `(verityFunction| function $[$modsBefore:verityMutability]* $[$pureMod?:pureMutabilityMarker]? $[$modsAfter:verityMutability]* $name:ident ($[$params:verityParam],*) $[$guard?:verityInitGuard]? $[$modifierUse?:verityModifierUse]? $[$requiresRoleClause?:verityRequiresRole]? $[$modifiesClause?:verityModifies]? $[$localObligations?:verityLocalObligations]? : $retTy:term := $body:term) => do
+      let mut_ ← parseMutabilityModifiers (modsBefore ++ modsAfter) stx
+      let mut_ := { mut_ with isPure := pureMod?.isSome }
       let parsedParams ← params.mapM (parseParam newtypes structDecls adtDecls)
       let parsedReturnTy ← valueTypeFromSyntax newtypes structDecls adtDecls retTy
       match parsedReturnTy with
@@ -1187,6 +1190,7 @@ private def parseFunction (newtypes : Array NewtypeDecl) (structDecls : Array St
         returnTy := parsedReturnTy
         isPayable := mut_.isPayable
         isView := mut_.isView
+        isPure := mut_.isPure
         noExternalCalls := mut_.noExternalCalls
         allowPostInteractionWrites := mut_.allowPostInteractionWrites
         nonReentrantLock := mut_.nonReentrantLock
@@ -7438,6 +7442,7 @@ private def mkSpecCommand
       let localObligationTerms ← fn.localObligations.mapM mkModelLocalObligationTerm
       let payableTerm ← if fn.isPayable then `(true) else `(false)
       let viewTerm ← if fn.isView then `(true) else `(false)
+      let pureTerm ← if fn.isPure then `(true) else `(false)
       let noExternalCallsTerm ← if fn.noExternalCalls then `(true) else `(false)
       let allowPostInteractionWritesTerm ← if fn.allowPostInteractionWrites then `(true) else `(false)
       let nonReentrantLockTerm ← match fn.nonReentrantLock with
@@ -7457,6 +7462,7 @@ private def mkSpecCommand
         «returns» := $returnsTerm
         isPayable := $payableTerm
         isView := $viewTerm
+        isPure := $pureTerm
         noExternalCalls := $noExternalCallsTerm
         allowPostInteractionWrites := $allowPostInteractionWritesTerm
         nonReentrantLock := $nonReentrantLockTerm
@@ -7483,6 +7489,7 @@ private def mkSpecCommand
         «returns» := []
         isPayable := false
         isView := false
+        isPure := false
         noExternalCalls := false
         allowPostInteractionWrites := false
         nonReentrantLock := none
@@ -8053,6 +8060,8 @@ def validateFunctionDeclsPublic
     -- view functions must not use modifies (they already imply no writes)
     if fn.isView && !fn.modifies.isEmpty then
       throwErrorAt fn.ident s!"function '{fn.name}' is marked view and modifies(...); view already guarantees no state writes"
+    if fn.isPure && !fn.modifies.isEmpty then
+      throwErrorAt fn.ident s!"function '{fn.name}' is marked pure and modifies(...); pure already guarantees no state writes"
     -- Validate nonreentrant lock field references a valid storage field of scalar uint256 type
     match fn.nonReentrantLock with
     | some lockField =>
@@ -8097,6 +8106,7 @@ def mkFunctionCommandsPublic
   let localObligationTerms ← fn.localObligations.mapM mkModelLocalObligationTerm
   let payableTerm ← if fn.isPayable then `(true) else `(false)
   let viewTerm ← if fn.isView then `(true) else `(false)
+  let pureTerm ← if fn.isPure then `(true) else `(false)
   let noExternalCallsTerm ← if fn.noExternalCalls then `(true) else `(false)
   let allowPostInteractionWritesTerm ← if fn.allowPostInteractionWrites then `(true) else `(false)
   let nonReentrantLockTerm ← match fn.nonReentrantLock with
@@ -8119,6 +8129,7 @@ def mkFunctionCommandsPublic
     «returns» := $returnsTerm
     isPayable := $payableTerm
     isView := $viewTerm
+    isPure := $pureTerm
     noExternalCalls := $noExternalCallsTerm
     allowPostInteractionWrites := $allowPostInteractionWritesTerm
     nonReentrantLock := $nonReentrantLockTerm

docs-site/content/edsl-api-reference.mdx

@@ -162,7 +162,7 @@ return (first, second)
 
 Tuple-typed parameters stay shape-preserved as right-nested Lean products; ABI-flattened aliases (`pair_0`, `pair_1`, …) are injected so you can use them directly. `_` binders are accepted and discarded hygienically.
 
-### Stateless contracts and payable / initializer constructors
+### Stateless contracts and mutability markers
 
 ```verity
 verity_contract Stateless where
@@ -180,6 +180,17 @@ constructor (seedOwner : Address) payable := do
 
 `payable` removes the `callvalue` guard and emits `stateMutability: "payable"` in the ABI.
 
+```verity
+function pure double (value : Uint256) : Uint256 := do
+  return (add value value)
+```
+
+`view` functions may read storage and the execution environment but cannot write state.
+`pure` functions cannot read or write state or environment values. Mutability checks include
+internal helper calls, so a `view` or `pure` wrapper is rejected if a helper it calls violates
+that marker. Generated ABI JSON emits `stateMutability: "view"` or `"pure"` for the matching
+function marker.
+
 ```verity
 function initOwner (seedOwner : Address) initializer(initializedVersion) : Unit := ...
 function upgradeToV2 ()                 reinitializer(initializedVersion, 2) : Unit := ...