Issues

G23: public state-variable getters cannot be hop targets (StorageSlot vs hopCallView)

bug

#2439

· Th0rgal opened

on Sep 23, 2026

#check_contract: fail-closed CEI treats every internal helper call as an interaction and a write, so faithful Solidity bodies need allow_post_interaction_writes almost everywhere (Pareto G22)

#2435

· Th0rgal opened

on Sep 19, 2026

macro/#check_contract: `let _ ← f` lowers to a `__discard` local that the compiler's reserved-prefix check rejects (Pareto G21)

#2434

· Th0rgal opened

on Sep 19, 2026

macro: zero-argument context-taking helper called as a bare statement is not threaded (Pareto G20)

#2431

· Th0rgal opened

on Sep 19, 2026

verity_contract bodies hit a Lean 4.31 do-notation elaboration failure (name-dependent) with mutable reassignments interleaved with binds

#2427

· Th0rgal opened

on Sep 18, 2026

Typed interface calls cannot return multiple values

#2424

· Th0rgal opened

on Sep 18, 2026

Ergonomics: Contracts namespace clashes, reserved identifiers (from/to/this), reserved ERC-20 helper names, callee-first ordering

#2423

· Th0rgal opened

on Sep 18, 2026

Auto view-frame proof fails on require/revert and static calls, forcing view markers to be dropped

#2422

· Th0rgal opened

on Sep 18, 2026

Statement/expression forms rejected in verity_contract bodies: if-without-else, mutable monadic rebinds, Int256/Bool ternaries, Bool negation

#2421

· Th0rgal opened

on Sep 18, 2026

Absolute parent slots and diamond rejection prevent reusing OZ upgradeable parents across inheritance chains

#2420

· Th0rgal opened

on Sep 18, 2026

override bodies are elaborated at the parent's position (cannot use child helpers); no super.f(args)

#2419

· Th0rgal opened

on Sep 18, 2026

Interface-typed storage fields are rejected (design note promises them); no address-to-interface cast for storage-held callees

#2418

· Th0rgal opened

on Sep 18, 2026

Navigation Menu

All issues

G23: public state-variable getters cannot be hop targets (StorageSlot vs hopCallView)

#check_contract: fail-closed CEI treats every internal helper call as an interaction and a write, so faithful Solidity bodies need allow_post_interaction_writes almost everywhere (Pareto G22)

macro/#check_contract: `let _ ← f` lowers to a `__discard` local that the compiler's reserved-prefix check rejects (Pareto G21)

macro: zero-argument context-taking helper called as a bare statement is not threaded (Pareto G20)

verity_contract bodies hit a Lean 4.31 do-notation elaboration failure (name-dependent) with mutable reassignments interleaved with binds

Typed interface calls cannot return multiple values

Ergonomics: Contracts namespace clashes, reserved identifiers (from/to/this), reserved ERC-20 helper names, callee-first ordering

Auto view-frame proof fails on require/revert and static calls, forcing view markers to be dropped

Statement/expression forms rejected in verity_contract bodies: if-without-else, mutable monadic rebinds, Int256/Bool ternaries, Bool negation

Absolute parent slots and diamond rejection prevent reusing OZ upgradeable parents across inheritance chains

override bodies are elaborated at the parent's position (cannot use child helpers); no super.f(args)

Interface-typed storage fields are rejected (design note promises them); no address-to-interface cast for storage-held callees

Search results