OP Mainnet permissions modelling in Prolog.

optimism.pl

:- discontiguous malicious/1.
:- discontiguous finalized_invalid_root/1.
:- discontiguous recovers/1.
:- discontiguous invalid_state/1.

% DEFINED IN PROXY

malicious_upgrade(proxy(_, Admin)) :- malicious(Admin).

% DEFINED IN MULTISIG (e.g. GNOSIS SAFE)

% if size is 1, then if the single owner is malicious, the multisig is malicious
malicious(multisig(_, [Owner], _)) :- malicious(Owner).
% if the size is 2, then if both owners are malicious, the multisig is malicious
malicious(multisig(_, [Owner1, Owner2], 2)) :- malicious(Owner1), malicious(Owner2).
% if the size is 1, then if the single owner is recovering, the multisig is recovering
recovers(multisig(_, [Owner], _)) :- recovers(Owner).

% DEFINED IN OPTIMISM PORTAL

% permissioned fallback mechanism
is_active(permissioned_game(_,_)) :- optimism_portal(_, Guardian, _), malicious(Guardian).
is_not_active(permissioned_game(_,_)) :- optimism_portal(_, Guardian, _), recovers(Guardian).
invalid_state(Name) :- optimism_portal(proxy(Name, _), _, Games), member(Game, Games), finalized_invalid_root(Game), is_active(Game), \+ is_not_active(Game).

% freeze mechanism
freeze(Name) :- optimism_portal(proxy(Name, _), Guardian, _), malicious(Guardian).
unfreeze(Name) :- optimism_portal(proxy(Name, _), Guardian, _), recovers(Guardian).
permanent_freeze(Name) :- optimism_portal(proxy(Name, _), _, _), freeze(Name), \+ unfreeze(Name).

% steal cases
steal(Name) :- optimism_portal(proxy(Name, Admin), _, _), malicious_upgrade(proxy(Name, Admin)).
steal(Name) :- optimism_portal(proxy(Name, _), _, _), invalid_state(Name).

% DEFINED IN PERMISSIONED GAME

finalized_invalid_root(permissioned_game(Proposer, Challenger)) :- malicious(Proposer), malicious(Challenger).

% DEFINED IN DEPUTY MULTISIG

% acts as a 1/2 multisig, but the multisig can remove the deputy
malicious(deputy_module(Multisig, _)) :- malicious(Multisig).
malicious(deputy_module(_, Deputy)) :- malicious(Deputy).
recovers(deputy_module(Multisig, _)) :- recovers(Multisig).

% FACTS

optimism_portal(
    proxy(
        'OptimismPortal',
        multisig('SuperchainProxyAdminOwner', ['SecurityCouncil', 'FoundationMultisig_1'], 2)
    ),
    deputy_module(multisig('GuardianMultisig', ['SecurityCouncil'], 1), 'FoundationMultisig_2'), % guardian
    [permissioned_game('PermissionedProposer', 'PermissionedChallenger')]
).

%malicious('FoundationMultisig_1').
malicious('SecurityCouncil').
malicious('PermissionedProposer').
malicious('PermissionedChallenger').
%malicious('FoundationMultisig_2').
%recovers('SecurityCouncil').
recovers('NONE').