fix: sync task template signatures with proven theorems

[Th0rgal]

Summary

Fixes 9 Generated task template files whose theorem signatures had drifted from the actual proven theorems in Proofs.lean. These were flagged by Codex and Cursor Bugbot in #18.

Issues fixed

• 4 files reference undefined stronglyAcyclic — RemoveOwnerInListReachable, RemoveOwnerOwnerListInvariant, SwapOwnerInListReachable, SwapOwnerOwnerListInvariant all reference stronglyAcyclic which has no definition in the codebase. Replaced with uniquePredecessor (defined in Specs.lean:142), which is what the actual proofs use.

• Unnecessary hypotheses removed — Several tasks included hPreAcyclic : acyclic s, hFreshInList : freshInList s owner, hNoSelfLoop, hOwnerNePrev, hOldNePrev that the proofs derive internally from ownerListInvariant + uniquePredecessor.

• Missing hypotheses added — hUniquePred : uniquePredecessor s, hPrevNZ : prevOwner ≠ zeroAddress, hZeroInert : next s zeroAddress = zeroAddress were missing from tasks but required by the actual proofs.

• Acyclicity tasks simplified — addOwner_acyclicity, removeOwner_acyclicity, swapOwner_acyclicity had unnecessary pre-state invariant hypotheses. Acyclicity is a tautology (proven by acyclic_generic for any state).

• InListReachable — Removed unused _hPreSentNZ hypothesis, matched conclusion form to proof.

Affected files (9 of 15 tasks)

Task	Change
AddOwnerAcyclicity	Remove hPreAcyclic, hFreshInList
AddOwnerOwnerListInvariant	Remove hAcyclic, hFreshInList
InListReachable	Remove _hPreSentNZ, match conclusion form
RemoveOwnerAcyclicity	Remove hPreAcyclic
RemoveOwnerInListReachable	Replace stronglyAcyclic → uniquePredecessor, add hPrevNZ/hZeroInert, remove hAcyclic
RemoveOwnerOwnerListInvariant	Replace stronglyAcyclic → uniquePredecessor, remove hAcyclic/hOwnerNePrev/hNoSelfLoop
SwapOwnerAcyclicity	Remove hPreAcyclic, hFresh
SwapOwnerInListReachable	Replace stronglyAcyclic → uniquePredecessor, use ownerListInvariant instead of inListReachable, add hPrevNZ/hZeroInert, remove hAcyclic/hOldNePrev/hFresh
SwapOwnerOwnerListInvariant	Replace stronglyAcyclic → uniquePredecessor, remove hAcyclic/hOldNePrev/hFresh/hNoSelfLoop

Test plan

• Verify lake build still succeeds (task files are template stubs, not compiled)
• Cross-reference each task signature with the corresponding theorem in Proofs.lean

---

Note

Low Risk
Changes only adjust generated Lean task template theorem signatures and comments to match existing proved theorems/invariants, without modifying contract logic. Risk is low, mainly around downstream tooling expecting the old hypothesis lists.

Overview
Updates the generated OwnerManagerReach task templates to match the proven theorem interfaces: removes unused preconditions (e.g. acyclic, freshInList, self-loop and inequality facts), drops an unused _hPreSentNZ, and standardizes conclusions to use the inline post-state expression.

Replaces references to the nonexistent stronglyAcyclic assumption with uniquePredecessor and adds missing required hypotheses (hPrevNZ, hZeroInert) for removeOwner/swapOwner reachability and invariant preservation tasks.

Simplifies the *_acyclicity tasks to require only Solidity guard-style hypotheses, documenting that acyclicity follows generically (acyclic_generic) rather than from pre-state invariants.

^{Reviewed by Cursor Bugbot for commit 54d6cb0. Bugbot is set up for automated code reviews on this repo. Configure here.}