module CONSTANTS (TYPES) is

function N: NAT is  -- number of nodes in the network (derived from type PID)
   ensure result > 0;
   return NAT (last of PID)
end function

function C: NAT is  -- committee size (parameter)
   ensure 0 < result and result <= N;
   return 3
end function

function H: NAT is  -- number of honest nodes (parameter)
   ensure 0 <= result and result <= N;
   return 2  -- 2 for configuration A_(2,2), 4 for configuration A_(4,0)
end function

function T: NAT is  -- threshold of votes needed to commit a block (parameter)
   ensure result >= (2 * (C + 1)) div 3;  -- i.e., (2 / 3) * C, rounded up
   return 2
end function

function P_V: PROB is  -- probability that a node is selected for the committee
   return PROB (REAL (C) / REAL (N))
end function

function P_H: PROB is  -- probability that an elected leader is honest
   var P: REAL in
      P := REAL (H) / REAL (N);  -- probability that a node is honest
      return PROB ((P ^ 2.0) * (1.0 + P - (P ^ 2.0)))  -- from Chen-Micali-19
   end var
end function

end module