Example of using clingo for model checking a protocol defined with logical clasues

gistfile1.txt

%*******************************************************************************%
%******************************** EXECUTION ************************************%
%*******************************************************************************%

do(act_sign_config(ConfigHash), A, T) :-
	posted(config(ConfigHash, _, _, SelfT, A), T),
	not posted(config_signature(ConfigHash, A), T),
	not pending(_, A, T),
	active(A, T), a(A).

do(act_post_share(ConfigHash, Contest), A, T) :-
    posted(config(ConfigHash, _, _, SelfT, A), T),
	contest(ConfigHash, Contest, T),
	config_ok(ConfigHash, T),
	not posted(pk_share(ConfigHash, Contest, _, SelfT), T),
	not pending(_, A, T),
	active(A, T), a(A).

do(act_combine_shares(ConfigHash, Contest, Hashes), A, T) :-
    posted(config(ConfigHash, _, _, 0, A), T),
	config_ok(ConfigHash, T),
	pk_shares_ok(ConfigHash, Contest, Hashes, T),
    not posted(pk_signature(ConfigHash, Contest, _, 0), T),
	not pending(_, A, T),
	active(A, T), a(A).

do(act_sign_pk(ConfigHash, Contest, PkHash, Hashes), A, T) :-
	posted(config(ConfigHash, _, _, SelfT, A), T),
	config_ok(ConfigHash, T),
	pk_shares_ok(ConfigHash, Contest, Hashes, T),
	posted(pk_signature(ConfigHash, Contest, PkHash, 0), T),
    not posted(pk_signature(ConfigHash, Contest, PkHash, SelfT), T),
	not pending(_, A, T),
	active(A, T), a(A).

do(act_mix(ConfigHash, Contest, BallotsHash, PkHash), A, T) :-
	pk_ok(ConfigHash, Contest, PkHash, T),
	posted(config(ConfigHash, _, _, 0, A), T),
	config_ok(ConfigHash, T),
	posted(ballots(ConfigHash, Contest, BallotsHash), T),
	not posted(mix_signature(ConfigHash, Contest, _, _, 0, 0), T),
	not pending(_, A, T),
	active(A, T), a(A).

do(act_mix(ConfigHash, Contest, MixBallotsHash, PkHash), A, T) :-
	pk_ok(ConfigHash, Contest, PkHash, T),
	posted(config(ConfigHash, _, _, SelfT, A), T),
	config_ok(ConfigHash, T),
	SelfT > 0,
	% the previous mix was signed by its producer
	posted(mix_signature(ConfigHash, Contest, MixBallotsHash, _, SelfT - 1, SelfT - 1), T),
	% we have verified the previous mix
	posted(mix_signature(ConfigHash, Contest, MixBallotsHash, _, SelfT - 1, SelfT), T),
	not posted(mix_signature(ConfigHash, Contest, _, _, SelfT, SelfT), T),
	not pending(_, A, T),
	active(A, T), a(A).

% check mix 0
do(act_check_mix(ConfigHash, Contest, 0, MixHash, BallotsHash, PkHash), A, T) :-
	pk_ok(ConfigHash, Contest, PkHash, T),
	posted(config(ConfigHash, _, _, SelfT, A), T),
	config_ok(ConfigHash, T),
	% the mix to verify
	posted(mix_signature(ConfigHash, Contest, MixHash, BallotsHash, 0, 0), T),
	% input ballots to mix came from the ballotbox
	posted(ballots(ConfigHash, Contest, BallotsHash), T),
	not posted(mix_signature(ConfigHash, Contest, MixHash, BallotsHash, 0, SelfT), T),
	not pending(_, A, T),
	active(A, T), a(A).

% check mix n
do(act_check_mix(ConfigHash, Contest, MixerT, MixHash, MixBallotsHash, PkHash), A, T) :-
	pk_ok(ConfigHash, Contest, PkHash, T),
	posted(config(ConfigHash, _, _, SelfT, A), T),
	config_ok(ConfigHash, T),
	% the mix to verify
	posted(mix_signature(ConfigHash, Contest, MixHash, MixBallotsHash, MixerT, SignerT), T),
	MixerT > 0,
	% input ballots to mix came from a previous mix, thus (mixer_t - 1)
	posted(mix_signature(ConfigHash, Contest, MixBallotsHash, _, MixerT - 1, SignerT), T),
	not posted(mix_signature(ConfigHash, Contest, MixHash, MixBallotsHash, MixerT, SelfT), T),
	not pending(_, A, T),
	active(A, T), a(A).

do(act_partial_decrypt(ConfigHash, Contest, MixHash, Share), A, T) :-
	pk_ok(ConfigHash, Contest, PkHash, T),
	posted(config(ConfigHash, _, _, SelfT, A), T),
	config_ok(ConfigHash, T),
	posted(pk_share(ConfigHash, Contest, Share, SelfT), T),
	contest_mixed_ok(ConfigHash, Contest, MixHash, T),
	not posted(decryption(ConfigHash, Contest, _, SelfT), T),
	not pending(_, A, T),
	active(A, T), a(A).

do(act_combine_decryptions(ConfigHash, Contest, Decryptions, MixHash, Shares), A, T) :-
	decryptions_ok(ConfigHash, Contest, Decryptions, T),
	posted(config(ConfigHash, _, _, 0, A), T),
	config_ok(ConfigHash, T),
	contest_mixed_ok(ConfigHash, Contest, MixHash, T),
	pk_shares_ok(ConfigHash, Contest, Shares, T),
	not posted(plaintexts_signature(ConfigHash, Contest, _, 0), T),
	not pending(_, A, T),
	active(A, T), a(A).

do(check_plaintexts(ConfigHash, Contest, PlaintextsHash, Decryptions, MixHash, Shares), A, T) :-
	decryptions_ok(ConfigHash, Contest, Decryptions, T),
	posted(config(ConfigHash, _, _, SelfT, A), T),
	config_ok(ConfigHash, T),
	contest_mixed_ok(ConfigHash, Contest, MixHash, T),
	pk_shares_ok(ConfigHash, Contest, Shares, T),
	posted(plaintexts_signature(ConfigHash, Contest, PlaintextsHash, 0), T),
	not posted(plaintexts_signature(ConfigHash, Contest, PlaintextsHash, SelfT), T),
	not pending(_, A, T),
	active(A, T), a(A).


%********** CONFIG **********%

config_ok(ConfigHash, T) :-
	posted(config(ConfigHash, _, TotalT, _, _), T),
	config_signed_upto(ConfigHash, TotalT - 1, T).

config_signed_upto(ConfigHash, 0, T) :-
	posted(config_signature(ConfigHash, 0), T).

config_signed_upto(ConfigHash, Trustee + 1, T) :-
    config_signed_upto(ConfigHash, Trustee, T),
    posted(config_signature(ConfigHash, Trustee + 1), T).

%********** SHARES **********%

pk_shares_ok(ConfigHash, Contest, Shares, T) :-
	posted(config(ConfigHash, _, TotalT, _, _), T),
	config_ok(ConfigHash, T),
	pk_shares_upto(ConfigHash, Contest, TotalT - 1, Shares, T).

pk_shares_upto(ConfigHash, Contest, 0, Share, T) :-
	posted(pk_share(ConfigHash, Contest, Share, 0), T).

pk_shares_upto(ConfigHash, Contest, Trustee + 1, @concat(Shares, Share), T) :-
    pk_shares_upto(ConfigHash, Contest, Trustee, Shares, T),
    posted(pk_share(ConfigHash, Contest, Share, Trustee + 1), T).


%********** PK SIGNATURES **********%

pk_ok(ConfigHash, Contest, PkHash, T) :-
	posted(config(ConfigHash, _, TotalT, _, _), T),
	config_ok(ConfigHash, T),
	pk_signed_upto(ConfigHash, Contest, PkHash, TotalT - 1, T).

pk_signed_upto(ConfigHash, Contest, PkHash, 0, T) :-
	posted(pk_signature(ConfigHash, Contest, PkHash, 0), T).

pk_signed_upto(ConfigHash, Contest, PkHash, Trustee + 1, T) :-
    pk_signed_upto(ConfigHash, Contest, PkHash, Trustee, T),
    posted(pk_signature(ConfigHash, Contest, PkHash, Trustee + 1), T).

%********** MIXES **********%

mix_ok(ConfigHash, Contest, MixHash, BallotsHash, T) :-
	posted(config(ConfigHash, _, TotalT, _, _), T),
	config_ok(ConfigHash, T),
	mix_signed_upto(ConfigHash, Contest, MixHash, BallotsHash, TotalT - 1, T).

mix_signed_upto(ConfigHash, Contest, MixHash, BallotsHash, 0, T) :-
	posted(mix_signature(ConfigHash, Contest, MixHash, BallotsHash, _, 0), T).

mix_signed_upto(ConfigHash, Contest, MixHash, BallotsHash, SignerT + 1, T) :-
	mix_signed_upto(ConfigHash, Contest, MixHash, BallotsHash, SignerT, T),
	posted(mix_signature(ConfigHash, Contest, MixHash, BallotsHash, _, SignerT + 1), T).

contest_mixed_ok(ConfigHash, Contest, MixHash, T) :-
	posted(config(ConfigHash, _, TotalT, _, _), T),
	config_ok(ConfigHash, T),
	contest_mixed_upto(ConfigHash, Contest, MixHash, TotalT - 1, T).

contest_mixed_upto(ConfigHash, Contest, MixHash, 0, T) :-
	mix_ok(ConfigHash, Contest, MixHash, BallotsHash, T),
	posted(ballots(ConfigHash, Contest, BallotsHash), T).

contest_mixed_upto(ConfigHash, Contest, MixHash, Trustee + 1, T) :-
	contest_mixed_upto(ConfigHash, Contest, PreviousMixHash, Trustee, T),
	mix_ok(ConfigHash, Contest, MixHash, PreviousMixHash, T).

%********** DECRYPTIONS **********%

decryptions_ok(ConfigHash, Contest, Decryptions, T) :-
	posted(config(ConfigHash, _, TotalT, _, _), T),
	config_ok(ConfigHash, T),
	decryptions_upto(ConfigHash, Contest, TotalT - 1, Decryptions, T).

decryptions_upto(ConfigHash, Contest, 0, Decryption, T) :-
	posted(decryption(ConfigHash, Contest, Decryption, 0), T).

decryptions_upto(ConfigHash, Contest, Trustee + 1, @concat(Decryptions, Decryption), T) :-
    decryptions_upto(ConfigHash, Contest, Trustee, Decryptions, T),
    posted(decryption(ConfigHash, Contest, Decryption, Trustee + 1), T).

%********** PLAINTEXTS **********%

plaintexts_ok(ConfigHash, Contest, PlaintextsHash, T) :-
	posted(config(ConfigHash, _, TotalT, _, _), T),
	config_ok(ConfigHash, T),
	plaintexts_signed_upto(ConfigHash, Contest, PlaintextsHash, TotalT - 1, T).

plaintexts_signed_upto(ConfigHash, Contest, PlaintextsHash, 0, T) :-
	posted(plaintexts_signature(ConfigHash, Contest, PlaintextsHash, 0), T).

plaintexts_signed_upto(ConfigHash, Contest, PlaintextsHash, Trustee + 1, T) :-
    plaintexts_signed_upto(ConfigHash, Contest, PlaintextsHash, Trustee, T),
    posted(plaintexts_signature(ConfigHash, Contest, PlaintextsHash, Trustee + 1), T).

%********** CONTEST **********%

contest(ConfigHash, Contests - 1, T) :-
	posted(config(ConfigHash, Contests, _, SelfT, _), T),
	t(T).
		
contest(ConfigHash, N - 1, T) :- contest(ConfigHash, N, T),
    N > 0.


%*******************************************************************************%
%******************************** SIMULATION ***********************************%
%*******************************************************************************%
#script (python)
from clingo import String

def concat(a, b):
	return String(a.string + "," + b.string)

def concat2(a, b):
	return String(a.string + "-" + str(b.number))
#end.

#const config_hash = "config_hash".

% in execution mode, A and T will be zero: a(0), t(0)
t(0..horizon).
a(0..auths - 1).

% The active predicate represents whether or not a given authority is active 
% for the duration of interval T.
%
% In execution mode, it is sufficient to set active(0, 0).
%
active(0..auths - 1, 0..horizon).
% represents a missing authority
% active(0..auths - 2, 0..horizon).

% Bootstrap protocol by adding config
%
% We're duplicating the A value so that each authority can select their particular
% configuration using that as an index, it just happens that the index
% is currently the only authority-specific information in the configuration
% In execution mode, A will be set to 0, so input fact parsing should
% include an extra 0 in the config predicate
posted_at(config(config_hash, contests, auths, A, A), -1, 0) :- a(A).
% Once the pk is posted, simulate posting ballots by the ballotbox at T + 1,
% we need the second predicate to only generate posted_at once, at T + 1
posted_at(ballots(ConfigHash, Contest, "ballots_hash"), -1, T + 1) :- 
	pk_ok(ConfigHash, Contest, PkHash, T),
	posted_at(pk_signature(_, _, _, _), _, T).

% Actions
% Pending work is work required by authority A when BB is at time T
% This could be due to
% authority A still has to update to T
% authority A still has to compute the work
% authority A still has to successfully send work back to BB
pending(config_signature(ConfigHash, A), A, T + 1) :- do(act_sign_config(ConfigHash), A, T).
pending(pk_share(ConfigHash, Contest, @concat2("share_hash_by", A), A), A, T + 1) :- do(act_post_share(ConfigHash, Contest), A, T).
pending(pk_signature(ConfigHash, Contest, @concat("combined", Hashes), A), A, T + 1) :- do(act_combine_shares(ConfigHash, Contest, Hashes), A, T).
pending(pk_signature(ConfigHash, Contest, PkHash, A), A, T + 1) :- do(act_sign_pk(ConfigHash, Contest, PkHash, Hashes), A, T).
pending(mix_signature(ConfigHash, Contest, @concat2("mix_hash_by", A), MixHash, A, A), A, T + 1) :- do(act_mix(ConfigHash, Contest, MixHash, PkHash), A, T).
pending(mix_signature(ConfigHash, Contest, MixHash, MixBallotsHash, MixerT, A), A, T + 1) :- do(act_check_mix(ConfigHash, Contest, MixerT, MixHash, MixBallotsHash, PkHash), A, T).
pending(decryption(ConfigHash, Contest, @concat2("decryption_hash_by", A), A), A, T + 1) :- do(act_partial_decrypt(ConfigHash, Contest, MixHash, Share), A, T).
pending(plaintexts_signature(ConfigHash, Contest, @concat("combined", Decryptions), A), A, T + 1) :- do(act_combine_decryptions(ConfigHash, Contest, Decryptions, MixHash, Shares), A, T).
pending(plaintexts_signature(ConfigHash, Contest, PlaintextsHash, A), A, T + 1) :- do(check_plaintexts(ConfigHash, Contest, PlaintextsHash, Decryptions, MixHash, Shares), A, T).

% pending work that has not been posted is still pending
pending(W, A, T + 1) :- not posted_at(W, A, T), pending(W, A, T), active(A, T + 1), t(T).

% Posting occurs non-deterministically modeling 3 factors
%
% 1) Synchronizing from BB is non-deterministic
% 2) Work completion time is non-deterministic
% 3) Sending to BB is non-deterministic
%
%  Additionally, only 1 post can occur on the BB hashchain at a certain point,
%  meaning posts will have to be retried (by the losers) if there is a conflict.
% 
% A choice is used to model this set of concurrent events
% such that a serial sequence of posts results
%
1 { select(0..auths - 1, T) } 1 :- pending(W, A, T), t(T).
:- select(A, T), not pending(_, A, T).

% chosen pending predicate is converted into a posted_at predicate, i.e. work is posted to the BB
posted_at(W, A, T) :- pending(W, A, T), select(A, T).

% integrity constraint: ensure that there is a successful post for each T at which 
% there is at least one post attempt. The last predicate is included to prevent 
% unsatisfiability in case the horizon does not reach the posted_at time
% :- not posted_at(_, _, T), pending(_, _, T), t(T).

% W was posted by time T if it was posted at T or earlier
% When running in execution mode, input facts must generate posted() predicates 
% with time 0 and auth 0: posted(W, 0, 0)
posted(W, T) :- posted_at(W, A, Past), Past <= T, t(T).

ok(T) :- plaintexts_ok(config_hash, 0..contests, _, T).

% PROVE COMPLETION
% remove solutions that complete at some point
% if the problem is unsatisfiable it means completion is guaranteed at t=horizon
:- ok(0..horizon).

% PROVE NON-COMPLETION
% remove solutions that have not completed by the horizon
% if the problem is unsatisfiable it means completion is impossible
% :- not ok(horizon).

% clingo braid.lp -n 0 -c auths=3 -c contests=10 -c horizon=25 -q -e cautious --parallel-mode 8

#const contests = 2.
#const auths = 3.
#const horizon = 30.

% #show.
#show ok/1.
% #show contest_mixed_ok/4.
% #show decryptions_ok/4.
% #show decryptions_upto/5.
% #show contest_mixed_upto/5.
% #show mix_ok/5.
% #show mix_signed_upto/6.
% #show plaintexts_ok/4.
% #show posted_at/3.
% #show pending/3.
% #show do/3.
% #show select/2.
% #show pk_shares_upto/5.
% #show pk_shares_ok/4.
% #show contest/3.
% #show config_signed_upto/3.
% #show config_ok/2.
% #show do/3.
% #show pk_signed_upto/5.
% #show pk_ok/4.
% #show ok/1.