Axis 2: Compile-time safety enforcement — CEI, access control, unsafe blocks

[Th0rgal]

Goal

Make the Verity compiler enforce safety rules that Solidity leaves to programmer discipline. Three features share a common pattern: the macro enforces a safety rule by default, and opt-out requires either a proof, a known-safe guard, or an explicit trust surface marker.

Parent issue: #1726 (Language design improvements)
Connects to: #1724 Wave 2 (control flow, modifiers)

---

Feature 1: CEI Enforcement with Proof-Based Opt-Out (P0)

Problem

Reentrancy remains the most iconic smart contract vulnerability class. The DAO hack ($60M, 2016), Rari Capital ($80M, 2022), and Orion Protocol ($3M, 2023) all exploited the same pattern: external calls before state updates. Solidity's mitigation is a convention (Checks-Effects-Interactions) and an opt-in library (`ReentrancyGuard`). Neither is enforced by the language.

What Verity Already Has

• `nonReentrant` primitive (`Verity/Core.lean:562`) using storage slot lock pattern
• `ReentrancyExample` contract that formally proves the vulnerable pattern cannot maintain the supply invariant, and the safe pattern provably does

Design: Hybrid Enforcement

Default behavior: The macro statically scans each function body. If any write statement (`set*`, `emit`, storage mutation) appears after an external call (`externalCall`, `call`, `staticcall`, `delegatecall`), it emits a compile-time error.

Escalation ladder for opt-out (from least to most trust):

Path A — Provide a Lean Proof (zero trust)

```
@[cei_safe by reentrancySafetyProof]
function complexWithdraw (amount : Uint256) : Unit := do
externalCall target "callback()" []
setStorage balanceSlot newBalance -- allowed: proof certifies safety
```

Where `reentrancySafetyProof` is a theorem of type:
```lean
theorem reentrancySafetyProof :
∀ s s', complexWithdraw_spec amount s s' →
invariant_preserved s s' := by ...
```

The proof is machine-checked by Lean's kernel. This is the gold standard opt-out.

Path B — Use `nonReentrant` Guard (low trust)

```
function withdraw (amount : Uint256) : Unit := do
nonReentrant lockSlot do
externalCall target "transfer()" [amount]
setStorage balanceSlot newBalance -- CEI relaxed inside nonReentrant
```

The macro recognizes `nonReentrant` as a known-safe wrapper and suppresses the CEI error inside its body. This appears in `--trust-report` as "guarded by nonReentrant".

Path C — Annotation (explicit trust surface)

```
@[allow_post_interaction_writes "reason: callback is to trusted oracle"]
function oracleUpdate () : Unit := do
...
```

Appears in `--trust-report`. Can be denied project-wide via `--deny-post-interaction-writes`.

Implementation Plan

1. Static analysis (`Macro/Translate.lean` or new `Macro/CEICheck.lean`): Walk function body AST, track whether we've seen an external call, error on writes after calls
2. Path A: Extend `@[cei_safe by name]` attribute — resolve `name` as a theorem in scope, type-check against expected signature
3. Path B: Pattern-match `nonReentrant lockSlot do ...` in the AST walker, mark inner body as CEI-exempt
4. Path C: `@[allow_post_interaction_writes "reason"]` attribute — skip CEI check, emit trust-report entry
5. Trust report integration: Add CEI entries to `--trust-report` output

Estimated effort: 2–3 weeks

---

Feature 2: `@[requires Role]` with Auto-Generated Theorems (P0)

Problem

Access control is the #1 cause of smart contract losses ($953.2M cumulative per Hacken 2025). Solidity relies on runtime `require(msg.sender == owner)` checks that developers can forget to add.

Design

```
verity_contract GatedToken where
roles
Owner : ownerSlot
Minter : minterSlot
Pauser : pauserSlot

storage
ownerSlot : Address := slot 0
minterSlot : Address := slot 1
pauserSlot : Address := slot 2

@[requires Minter]
function mint (to : Address, amount : Uint256) : Unit := do
...

@[requires Owner]
function setMinter (newMinter : Address) : Unit := do
setStorageAddr minterSlot newMinter

-- No role annotation = public function
function balanceOf (addr : Address) : Uint256 := do
...
```

What `@[requires Role]` Generates

1. Runtime require check (injected at function entry):
```lean
require (sender == getStorageAddr ownerSlot) "Not owner"
```

Compiles to Yul:
```yul
if iszero(eq(caller(), sload(ownerSlot))) { revert(...) }
```

2. Access control theorem (auto-generated):
```lean
theorem setMinter_requires_owner :
∀ s s' sender newMinter, setMinter_spec newMinter sender s s' →
sender = s.storage ownerSlot := by ...
```

This theorem is auto-provable because the macro inserted the require. Its value:

• Auditors: machine-checked guarantee of access control
• Composability: downstream proofs can assume this theorem
• Safety net: removing the annotation removes the theorem, breaking any dependent proof → compile-time failure

Extensions

• Multi-role: `@[requires Owner | Minter]` generates OR-check
• Role hierarchies: definable in `roles` block
• Custom role resolution: `Role : expr` where `expr` is an arbitrary expression

Implementation Plan

1. Syntax (`Macro/Syntax.lean`): Add `roles` section binding role names to storage slots/expressions
2. Attribute (`Macro/Translate.lean`): Parse `@[requires RoleName]`, look up role → slot binding
3. Code injection: Prepend `require (sender == getStorageAddr slot) "Not {role}"` to function body
4. Theorem generation: Generate `functionName_requires_roleName` theorem alongside the function spec
5. Validation: Error if a role name is used that wasn't declared in `roles` block

Estimated effort: 2–3 weeks

---

Feature 3: Explicit `unsafe` Blocks (P1)

Problem

`delegatecall`, inline assembly, raw storage access, and external calls are all available everywhere in Solidity with no distinction from safe code. There's no way to grep for "all the dangerous operations in this contract."

What Verity Already Has

• `localObligations` on functions/constructors for trust-surface marking
• `--trust-report` for machine-readable trust surface output
• `--deny-*` flags for fail-closed verification
• `SupportedSpec` gates that categorize operations by safety surface

Design

```
function upgradeImplementation (newImpl : Address) : Unit := do
@[requires Owner]
let currentImpl ← getStorage implSlot

unsafe "delegatecall to new implementation" do
delegatecall gas() newImpl 0 0 0 0

-- Back to safe code
setStorage implSlot newImpl
```

The `unsafe` keyword:

1. Syntactically mandatory for: `delegatecall`, raw `mstore` to arbitrary offsets, raw `sstore`, inline Yul, `rawLog`
2. Requires a string description — appears in `--trust-report`
3. Searchable/greppable in audit
4. Can be denied project-wide via `--deny-unsafe`

Implementation Plan

1. Syntax: Add `unsafe "reason" do ...` block to the expression/statement grammar
2. Validation (`Macro/Translate.lean`): Track "safe context" flag. Error if a restricted operation appears outside `unsafe`
3. Trust report: Each `unsafe` block → entry in `--trust-report` with location, reason, and contained operations
4. Deny flag: `--deny-unsafe` makes any `unsafe` block a compile error (for contracts that want to prove they're fully safe)
5. Map to existing infra: `unsafe` blocks generate `localObligations` entries

Estimated effort: 2–3 weeks

---

Shared Pattern: Escalation Ladder

All three features follow the same safety philosophy:

```
SAFE BY DEFAULT (compiler enforces)
↓ opt-out via:
LEAN PROOF (machine-checked, zero trust)
↓ if proof not feasible:
KNOWN-SAFE GUARD (nonReentrant, require, etc.)
↓ if guard not applicable:
EXPLICIT ANNOTATION (trust surface marker in --trust-report)
```

This gives developers clear escape hatches while keeping the default behavior strictly safe.

Execution Order

1. CEI enforcement (P0, 2–3 weeks) — highest impact per effort
2. `@[requires Role]` (P0, 2–3 weeks) — can be parallelized with CEI
3. `unsafe` blocks (P1, 2–3 weeks) — builds on trust-report infrastructure

Related Issues

• Language design improvements: fix Solidity's systemic flaws, inspired by Rust/Cairo/Move #1726 — Parent: language design improvements
• Solidity feature parity: close the gap between verity_contract EDSL and production Solidity #1724 — Solidity parity (Wave 2: modifiers, control flow)
• Extend proven fragment to cover the full CompilationModel language surface #1723 — Proven fragment extension (auto-generated theorems accelerate this)

[Th0rgal]

Scope update: #1731 attempts CEI/access-control/unsafe work, but this issue should stay open until CEI opt-outs are honest trust surfaces or proof-checked, nonReentrant guards are actually enforced/validated, and internal/expression-position calls are covered by the safety scans.

[Th0rgal]

Scope update after #1725/#1737:

This axis remains open. To keep the scope precise, safety features should be categorized as one of:

• hard compiler enforcement,
• verified opt-out through a checked proof or known guard,
• explicit trust surface reported by tooling.

cei_safe and nonreentrant(lock) should not silently bypass CEI unless the implementation either validates the proof/guard shape or records the bypass as trust surface. Internal calls and expression-position calls also need to be part of the analysis before the CEI/no-call checks can be considered complete.

Native EVMYulLean runtime targeting is tracked separately in #1737.

[Th0rgal]

Scope update after #1725:

This issue remains open. #1725 does not implement CEI enforcement, role/access-control theorem generation, or unsafe-block trust reporting.

For PRs against this issue, the remaining acceptance bar is that safety annotations are enforced honestly:

• CEI opt-outs must require a checked proof, a real recognized guard, or an explicit trust-surface marker.
• nonreentrant(lock) must insert or verify an actual lock discipline, not only silence CEI validation.
• internal calls, expression-position calls, and nested statements must be included in the analysis.

[Th0rgal]

Scope update after the current #1731 branch:

#1731 implements the first CEI/access-control/unsafe-block surface and now includes additional hardening from review:

• nonreentrant(field) and cei_safe no longer suppress CEI merely as metadata.
• internal calls are treated conservatively by modifies(...), no_external_calls, and CEI write checks.
• nested helper calls in compound statements are handled more conservatively.

Still remaining before this axis is complete:

• nonreentrant(field) should either synthesize/verify an actual lock acquire/release pattern, or remain explicitly metadata-only.
• cei_safe needs a real proof obligation or should be documented as a trust hook, not a CEI bypass.
• unsafe-block reporting and --deny-unsafe should be audited after Language design axes: full implementation (25 steps across 6 axes) #1731 merges.

Keep open until #1731 lands and those remaining semantics are split or finished.