1/*
    2Computing the probability of mining the next block with a two-phase
    3Proof-of-Work protocol in a Bitcoin network
    4From Damiano Azzolini, Fabrizio Riguzzi, Evelina Lamma, Elena Bellodi,
    5and Riccardo Zese.
    6Modeling bitcoin protocols with probabilistic logic programming.
    7PLP 2018 http://ceur-ws.org/Vol-2219/paper6.pdf
    8*/
    9:- use_module(library(mcintyre)).   10
   11:- if(current_predicate(use_rendering/1)).   12:- use_rendering(c3).   13:- use_rendering(graphviz).   14:- endif.   15
   16:- mc.   17
   18:- begin_lpad.   19
   20% http://referaat.cs.utwente.nl/conference/22/paper/7473/preventingthe-51-attack%20-a-stochastic-analysis-of-two-phase-proof-of-work-in-bitcoin.pdf
   21/*
   22 * 2-phase PoW. 
   23 * This new method consists of a PoW organized in 2 steps: 
   24 * the first step is to find a double hash of the header SHA256(SHA256(header)) 
   25 * that is smaller than a certain value X (this is the current PoW). 
   26 * The second one consists in signing the header with the private key of the 
   27 * address that will receive the mining reward and then finding a new hash 
   28 * SHA256(SIG(header,privateKey)) smaller than a value Y 
   29 * a peer can be in one of the following 4 states:
   30 * – State 0 (a0): a miner generates a hash using a certain nonce. 
   31 *		If this hash is correct, it will move to state 1, 
   32 *  	if it’s not, it will stay in a0.
   33 * – State 1 (a1): the miner has already solved the first hash 
   34 *		puzzle (he has found a nonce value such that SHA256(SHA256(header)) 
   35 *	   	is less than a difficulty parameter X) and now needs to solve 
   36 *		the second one (find a hash value such that SHA256(SIG(header,privateKey)) 
   37 *      is less than a difficulty parameter Y). 
   38 * – State 2 (a2): the miner has solved both hashes, is rewarded and now 
   39 *  	is ready to mine another block (back to state 0). 
   40 * – State 3 (a3): another miner has solved the second hash, 
   41 * 		so the first miner can now stop working on this hash and move 
   42 *	    to another one (back to state 0).
   43*/
   44
   45reach(S, I, T) :-
   46  	trans(S, I, U),
   47  	reach(U, next(I), T).
   48reach(S, _, S).
   49
   50a_found_y(_):0.15.
   51b_found_y(_):0.25.
   52b_found_x(_):0.10.
   53found_y(S):- a_found_y(S); b_found_y(S).
   54
   55trans(a0,S,a1):1.0/50; trans(a0,S,a0):1.0-1.0/50:- \+b_found_x(S).
   56
   57
   58trans(a1,S,a2):0.15;trans(a1,S,a1):1.0-0.15:- \+b_found_y(S).
   59
   60trans(a0,S,a3):- b_found_x(S).
   61trans(a1,S,a3):- b_found_y(S).
   62
   63trans(a2,S,a0):- a_found_y(S).
   64trans(a3,S,a0):- b_found_y(S).
   65
   66% same for B
   67trans(b0,S,b1):1.0/28; trans(b0,S,b0):1.0-1.0/28:- \+a_found_y(S).
   68trans(b1,S,b2):0.25;trans(b1,S,b1):1.0-0.25:- \+a_found_y(S).
   69trans(b0,S,b3):- a_found_y(S).
   70trans(b1,S,b3):- a_found_y(S).
   71
   72trans(b2,S,b0):- a_found_y(S).
   73trans(b3,S,b0):- b_found_y(S).
   74
   75:- end_lpad.   76
   77draw(D):-
   78    runModel(1000,PA,_),
   79    histogram(PA,D,[nbins(100)]).
   80
   81% used to draw the graph
   82runModel(0,[],[]).
   83runModel(I,[[PA]-1|TA],[[_]-1|TB]):-
   84    I > 0,
   85    mc_sample(reach(a0,0,a2),100,PA),
   86    %mc_sample(reach(b0,0,b2),100,PB),
   87    I1 is I-1,
   88    runModel(I1,TA,TB).
   89markov_chain(digraph(G)):-
   90    findall(edge(A -> B,[label=P]),
   91            (clause(trans(A,_,B),
   92                    (sample_head(_,_,Probs,N))),
   93                nth0(N,Probs,_:P)),
   94            G0),
   95    findall(edge(A -> B,[label=1.0]),
   96            clause(trans(A,_,B),_),
   97            G1),
   98    append(G0,G1,G).