Goal
Turn Verity's mutability annotations into a full effect system where each annotation is both verified at compile time and auto-generates frame condition theorems that downstream proofs can use. This is the bridge between the EDSL and the proof system, and directly accelerates #1723 (proven fragment extension).
Parent issue: #1726 (Language design improvements)
Connects to: #1724 Wave 2 (modifiers), #1723 (proven fragment extension)
Current State
Verity already has `@[view]` and `@[payable]` annotations:
- `@[payable]` generates a runtime `callvalue` guard (`CodegenCommon.lean:60-74`). When `isPayable = false`, the dispatcher prepends `if callvalue() { revert(0, 0) }`. This is a real runtime guard.
- `@[view]` triggers compile-time validation (`Validation.lean:398-411`). The `stmtWritesState` function recursively checks every statement for storage writes, mapping writes, event emissions, and external calls. If any are found in a `view` function, compilation fails.
- Neither generates proof obligations or frame condition theorems. The annotations are boolean flags on `FunctionSpec` (`isPayable`, `isView`, `isPure`).
What's Missing
Frame condition theorems are the bottleneck in compositional verification. Today, you write them by hand in `Spec.lean` files using `#gen_spec` macros. For example, `sameStorageMap2Context` asserts that mapping storage, double-mapping storage, arrays, and context are all unchanged.
If `@[view]` auto-generated a theorem saying "this function preserves all state", that theorem could be used by any downstream proof that calls the view function — eliminating manual frame condition boilerplate.
Design: Three Annotation Levels
Level 1: `@[view]` — No State Modification
Already verified at compile time. Enhancement: auto-generate a frame theorem.
```
@[view]
function balanceOf (addr : Address) : Uint256 := do
getMapping balancesSlot addr
```
Auto-generated theorem:
```lean
theorem balanceOf_is_view :
∀ addr s s', balanceOf_spec addr s s' →
s'.storage = s.storage ∧
s'.storageArray = s.storageArray ∧
s'.events = s.events ∧
s'.transientStorage = s.transientStorage := by rfl
```
This is provable by `rfl` because the function body only reads — the compiled code never calls `sstore` or `log`.
Level 2: `@[modifies slot1, slot2, ...]` — Bounded Mutation
New annotation. The function may write state, but only to the declared slots.
```
@[modifies balancesSlot, totalSupplySlot]
function transfer (to : Address, amount : Uint256) : Unit := do
let sender ← msgSender
let senderBal ← getMapping balancesSlot sender
require (senderBal >= amount) "Insufficient balance"
setMapping balancesSlot sender (sub senderBal amount)
setMapping balancesSlot to (add (getMapping balancesSlot to) amount)
-- Writing to ownerSlot here would be a COMPILE ERROR
```
Compile-time check: The macro enumerates all `set*` targets in the function body and verifies each target is in the declared set. Error if a write targets an undeclared slot.
Auto-generated theorem:
```lean
theorem transfer_frame :
∀ to amount s s', transfer_spec to amount s s' →
∀ slot, slot ≠ balancesSlot.slot → slot ≠ totalSupplySlot.slot →
s'.storage slot = s.storage slot := by ...
```
This is the exact frame condition shape that `#gen_spec` macros produce today (e.g., `storageUnchangedExcept`). The annotation automates what developers currently specify manually.
Level 3: `@[no_external_calls]` — Reentrancy-Safe by Construction
New annotation. The function makes no external calls, guaranteeing it cannot be a reentrancy vector.
```
@[no_external_calls]
function internalAccounting (amount : Uint256) : Unit := do
let balance ← getMapping balancesSlot sender
setMapping balancesSlot sender (add balance amount)
setStorage totalSupplySlot (add totalSupply amount)
```
Compile-time check: Reject any `externalCall`, `call`, `staticcall`, `delegatecall`, `ecm` in the body.
Auto-generated theorem:
```lean
theorem internalAccounting_no_calls :
∀ amount s s', internalAccounting_spec amount s s' →
noExternalCallsInExecution s s' := by ...
```
How This Connects to `#gen_spec`
The `#gen_spec` family of macros currently generates specs of this shape:
```lean
def constructor_spec (initialOwner : Address) (s s' : ContractState) : Prop :=
Verity.Specs.storageAddrStorageUpdateSpec 0 1
(fun _ => initialOwner) (fun _ => 0) sameStorageMap2Context s s'
```
This unfolds to: slot 0 gets `initialOwner`, slot 1 gets 0, all other slots unchanged, mapping/array/context unchanged.
Effect annotations produce the same information from a different angle:
- `#gen_spec` says: "here are the slots that change and their new values"
- `@[modifies]` says: "only these slots can change" (without specifying values)
They're complementary. `@[modifies]` gives a cheap frame condition for functions where you don't need to specify exact values. `#gen_spec` gives precise post-conditions when you do.
Annotation Composition
Annotations compose naturally:
```
@[view, no_external_calls] -- pure read, no calls
function getBalance (addr : Address) : Uint256 := do ...
@[modifies balancesSlot, no_external_calls] -- bounded writes, no calls
function internalTransfer (from to : Address, amount : Uint256) : Unit := do ...
@[modifies balancesSlot, totalSupplySlot] -- bounded writes, may call externally
function mint (to : Address, amount : Uint256) : Unit := do ...
```
Each combination generates the conjunction of the individual theorems.
Implementation Plan
Phase 1: Strengthen `@[view]` (1 week)
- Keep existing compile-time validation in `Validation.lean`
- Add theorem generation in `Macro/Elaborate.lean`: emit `functionName_is_view` theorem
- Theorem is provable by `rfl` — the spec's state components are equal
Phase 2: Add `@[modifies]` (2–3 weeks)
- Parse `@[modifies slot1, slot2, ...]` from function annotations
- New validation pass: walk body, collect all write targets, compare against declared set
- Generate `functionName_frame` theorem with universally quantified "unchanged" slots
- The theorem proof requires showing that the compiled function only touches declared slots — may need a simple tactic or be dischargeable by `simp`
Phase 3: Add `@[no_external_calls]` (1 week)
- Parse `@[no_external_calls]` annotation
- Validate: reject external call statements in body
- Generate `functionName_no_calls` theorem
Phase 4: Composition (1 week)
- Allow multiple annotations on a single function
- Generate conjunction theorem when multiple annotations are present
- Integration test: verify generated theorems are usable in downstream proofs
Total estimated effort: 3–4 weeks
Impact on Proven Fragment (#1723)
Auto-generated frame theorems directly unblock compositional proofs:
- Today: Proving `transfer` preserves `ownerSlot` requires manually writing the frame condition
- After: `@[modifies balancesSlot, totalSupplySlot]` generates the frame condition automatically — the proof of `ownerSlot` preservation is a one-liner applying `transfer_frame`
This means every function with an effect annotation automatically contributes to the proven fragment. As developers add annotations to existing contracts, the verification coverage grows with zero manual proof effort.
Related Issues
Goal
Turn Verity's mutability annotations into a full effect system where each annotation is both verified at compile time and auto-generates frame condition theorems that downstream proofs can use. This is the bridge between the EDSL and the proof system, and directly accelerates #1723 (proven fragment extension).
Parent issue: #1726 (Language design improvements)
Connects to: #1724 Wave 2 (modifiers), #1723 (proven fragment extension)
Current State
Verity already has `@[view]` and `@[payable]` annotations:
What's Missing
Frame condition theorems are the bottleneck in compositional verification. Today, you write them by hand in `Spec.lean` files using `#gen_spec` macros. For example, `sameStorageMap2Context` asserts that mapping storage, double-mapping storage, arrays, and context are all unchanged.
If `@[view]` auto-generated a theorem saying "this function preserves all state", that theorem could be used by any downstream proof that calls the view function — eliminating manual frame condition boilerplate.
Design: Three Annotation Levels
Level 1: `@[view]` — No State Modification
Already verified at compile time. Enhancement: auto-generate a frame theorem.
```
@[view]
function balanceOf (addr : Address) : Uint256 := do
getMapping balancesSlot addr
```
Auto-generated theorem:
```lean
theorem balanceOf_is_view :
∀ addr s s', balanceOf_spec addr s s' →
s'.storage = s.storage ∧
s'.storageArray = s.storageArray ∧
s'.events = s.events ∧
s'.transientStorage = s.transientStorage := by rfl
```
This is provable by `rfl` because the function body only reads — the compiled code never calls `sstore` or `log`.
Level 2: `@[modifies slot1, slot2, ...]` — Bounded Mutation
New annotation. The function may write state, but only to the declared slots.
```
@[modifies balancesSlot, totalSupplySlot]
function transfer (to : Address, amount : Uint256) : Unit := do
let sender ← msgSender
let senderBal ← getMapping balancesSlot sender
require (senderBal >= amount) "Insufficient balance"
setMapping balancesSlot sender (sub senderBal amount)
setMapping balancesSlot to (add (getMapping balancesSlot to) amount)
-- Writing to ownerSlot here would be a COMPILE ERROR
```
Compile-time check: The macro enumerates all `set*` targets in the function body and verifies each target is in the declared set. Error if a write targets an undeclared slot.
Auto-generated theorem:
```lean
theorem transfer_frame :
∀ to amount s s', transfer_spec to amount s s' →
∀ slot, slot ≠ balancesSlot.slot → slot ≠ totalSupplySlot.slot →
s'.storage slot = s.storage slot := by ...
```
This is the exact frame condition shape that `#gen_spec` macros produce today (e.g., `storageUnchangedExcept`). The annotation automates what developers currently specify manually.
Level 3: `@[no_external_calls]` — Reentrancy-Safe by Construction
New annotation. The function makes no external calls, guaranteeing it cannot be a reentrancy vector.
```
@[no_external_calls]
function internalAccounting (amount : Uint256) : Unit := do
let balance ← getMapping balancesSlot sender
setMapping balancesSlot sender (add balance amount)
setStorage totalSupplySlot (add totalSupply amount)
```
Compile-time check: Reject any `externalCall`, `call`, `staticcall`, `delegatecall`, `ecm` in the body.
Auto-generated theorem:
```lean
theorem internalAccounting_no_calls :
∀ amount s s', internalAccounting_spec amount s s' →
noExternalCallsInExecution s s' := by ...
```
How This Connects to `#gen_spec`
The `#gen_spec` family of macros currently generates specs of this shape:
```lean
def constructor_spec (initialOwner : Address) (s s' : ContractState) : Prop :=
Verity.Specs.storageAddrStorageUpdateSpec 0 1
(fun _ => initialOwner) (fun _ => 0) sameStorageMap2Context s s'
```
This unfolds to: slot 0 gets `initialOwner`, slot 1 gets 0, all other slots unchanged, mapping/array/context unchanged.
Effect annotations produce the same information from a different angle:
They're complementary. `@[modifies]` gives a cheap frame condition for functions where you don't need to specify exact values. `#gen_spec` gives precise post-conditions when you do.
Annotation Composition
Annotations compose naturally:
```
@[view, no_external_calls] -- pure read, no calls
function getBalance (addr : Address) : Uint256 := do ...
@[modifies balancesSlot, no_external_calls] -- bounded writes, no calls
function internalTransfer (from to : Address, amount : Uint256) : Unit := do ...
@[modifies balancesSlot, totalSupplySlot] -- bounded writes, may call externally
function mint (to : Address, amount : Uint256) : Unit := do ...
```
Each combination generates the conjunction of the individual theorems.
Implementation Plan
Phase 1: Strengthen `@[view]` (1 week)
Phase 2: Add `@[modifies]` (2–3 weeks)
Phase 3: Add `@[no_external_calls]` (1 week)
Phase 4: Composition (1 week)
Total estimated effort: 3–4 weeks
Impact on Proven Fragment (#1723)
Auto-generated frame theorems directly unblock compositional proofs:
This means every function with an effect annotation automatically contributes to the proven fragment. As developers add annotations to existing contracts, the verification coverage grows with zero manual proof effort.
Related Issues