{name}
+ {constraint}
+ + + {source} + +
+{children}
+
+ {formal}
+
+ ))}
+
+ The owners mapping forms a proper loop-free linked list starting at
+ a special node called{' '}
+
+ SENTINEL
+
+ , and the owners are exactly the addresses on that list.
+
{name}
- {constraint}
- - - {source} - -
-{children}
-
+ The{' '}
+
+ owners: address → address
+
+ . A sentinel node at address{' '}
+ 0x1 anchors
+ the list. All four ownership-mutating functions are modeled:
+
+ {'setupOwners \u2192 build initial list\n'}
+ {'addOwner \u2192 insert at head\n'}
+ {'removeOwner \u2192 unlink node\n'}
+ {'swapOwner \u2192 atomic replacement'}
+
+
+ The Safe is the most widely used multi-signature wallet on
+ Ethereum, securing billions of dollars. If the owners list in{' '}
+
+ The owners mapping forms a proper loop-free linked list
+ starting at a special node called{' '}
+ SENTINEL, and
+ the owners are exactly the addresses on that list.
+
+ In Lean, that goal is split into four named properties: +
+inListReachable
+ : every node with a non-zero successor is reachable from
+ SENTINEL
+ ownerListInvariant
+ : membership (non-zero successor) is equivalent to
+ reachability from SENTINEL (combines{' '}
+ inListReachable and{' '}
+ reachableInList)
+ acyclic: the
+ linked list has no SENTINEL cycles
+ stronglyAcyclic
+ : reachability is antisymmetric (no cycles at all)
+
+ These correspond to invariants from Certora's{' '}
+
+ The ownership operations are modeled in Verity from the Solidity{' '}
+
+ Reachability is expressed using witness chains: a
+ concrete list of addresses where each consecutive pair follows
+ the{' '}
+ owners{' '}
+ mapping. This turns the transitive closure into induction on
+ list indices, making the proof mechanically checkable.
+
+ For{' '}
+ removeOwner{' '}
+ and{' '}
+ swapOwner,
+ the proofs require strong acyclicity{' '}
+ (antisymmetry of the reachability relation) to show that
+ excising or replacing a node does not orphan downstream
+ nodes. This matches Certora's{' '}
+ reach_invariant{' '}
+ axiom.
+
+ Reference proofs are provided in{' '}
+
+ If the build succeeds, the proofs are correct.{' '}
+
+ 9 of 12 theorems are proven. The remaining three{' '}
+ ownerListInvariant{' '}
+ preservation theorems remain open in{' '}
+
| Function | +inListReachable | +ownerListInvariant | +acyclicity | +
|---|---|---|---|
| setupOwners | +proven | +proven | +proven | +
| addOwner | +proven | +open | +proven | +
| removeOwner | +proven | +open | +proven | +
| swapOwner | +proven | +open | +proven | +
+ The proofs use zero axioms. Each theorem requires hypotheses + drawn from the function's preconditions and structural + properties of the linked list. The hypotheses vary by function: +
+require guards
+ in every ownership-mutating function.
+ addOwner and{' '}
+ swapOwner.
+ removeOwner{' '}
+ and{' '}
+ swapOwner to
+ verify the caller supplied the right predecessor.
+ setupOwners{' '}
+ is the base case and does not require this hypothesis.
+ setupOwners{' '}
+ and{' '}
+ addOwner.
+ Used as a hypothesis for{' '}
+ removeOwner{' '}
+ and{' '}
+ swapOwner.
+ removeOwner{' '}
+ and{' '}
+ swapOwner{' '}
+ to ensure that excising or replacing a node doesn't
+ orphan downstream nodes through non-SENTINEL cycles.
+ removeOwner.
+ swapOwner,
+ the old owner cannot be its own predecessor. A self-loop
+ would cause the if-chain in the storage map to zero out the
+ previous owner's pointer, orphaning the new owner.
+
+ setupOwners{' '}
+ additionally requires a{' '}
+ hClean{' '}
+ hypothesis (all storage slots are zero) to ensure no stale
+ mappings from a prior state.
+
+
+
+ + What is a formal proof? + {' '} + A short explanation for non-specialists. +
+