project to automate the modeling of a smart contract as a game
#!/usr/bin/env python3
"""
input: json version of act specification;
       constraints on the initial state
output: a tree of possible function calls
"""
from __future__ import annotations

from abc import ABCMeta, abstractmethod
import itertools
import json
from act_ast import Contract, LitBool, And
from parse_act import parse_act_json


from typing import Any, Dict, Iterable, List, Union
import z3

#path = input("path to json respresenation of act specification\n")
#path = "act_examples/smoke/smoke.act.typed.json"
#path = "act_examples/token/transfer.act.typed.json"
from sys import argv
path = argv[1]

obj = json.load(open(path))




act = parse_act_json(obj)



# considered_contract = Contract(contracts[0])

# print(considered_contract)

x=LitBool(True)
y=And(x, x)

z = And(LitBool(True), LitBool(True))
    
print(z)
act2tree.py
sophierain/contract2game
from __future__ import annotations

from abc import ABCMeta, abstractmethod
from dataclasses import dataclass
from typing import Dict, List




# --- top level classes ---

@dataclass
class Act:
    store: Storage
    contracts: List[Contract]



@dataclass
class Contract:
    name: str
    constructor: Constructor
    behaviors: List[Behavior]

@dataclass
class Constructor:
    interface: Interface
    initial_storage: List[BoolExp]
    preConditions: List[BoolExp]
    postConditions: List[BoolExp]
    invariants: List[BoolExp]

@dataclass
class Behavior:
    """one function within a contract in a given case"""
    name: str
    interface: Interface
    caseConditions: List[BoolExp]
    preConditions: List[BoolExp]
    postConditions: List[BoolExp]
    returnValue: Exp 
    stateUpdates: List[BoolExp] #equality constraints e.g. update






# --- Interface ---
@dataclass
class Interface:
    name: str
    args: List[Decl]

@dataclass
class Decl:
    name: str
    type: AbiType






# --- Slot Types ---
class SlotType(metaclass=ABCMeta):
    """base class for storage variables"""

# --- Mapping Types ---
@dataclass
class MappingType(SlotType):
    argsType: List[ValueType]
    resultType: ValueType


class ValueType(SlotType, metaclass=ABCMeta):
    """base class for storage base variables"""

"""A description of the shape of global storage"""
Storage = Dict[str, Dict[str, SlotType]]


@dataclass
class ContractType(ValueType):
    contract: str

# --- Abi Types ---

@dataclass
class AbiType(ValueType, metaclass=ABCMeta):
    """base class for solidity abi types"""

@dataclass
class AbiUIntType(AbiType):
    size: int

@dataclass
class AbiIntType(AbiType):
    size: int

@dataclass
class AbiAddressType(AbiType):
    """address type"""

@dataclass
class AbiBoolType(AbiType):
    """bool type"""

@dataclass
class AbiBytesType(AbiType):
    size: int

@dataclass
class AbiBytesDynamicType(AbiType):
    """dynamic bytes type"""

@dataclass
class AbiStringType(AbiType):
    """string type"""

@dataclass
class AbiArrayDynamicType(AbiType):
    arraytype: AbiType

@dataclass
class AbiArrayType(AbiType):
    size: int
    arraytype: AbiType

@dataclass
class AbiTupleType(AbiType):
    tuple: List[AbiType]

@dataclass
class AbiFunctionType(AbiType):
    """function type"""






# --- expressions ---

class Exp(metaclass=ABCMeta):
    """base class for expressions"""

class IntExp(Exp, metaclass=ABCMeta):
    """integer expressions"""

class BoolExp(Exp, metaclass=ABCMeta):
    """boolean expressions"""

@dataclass
class LitBool(BoolExp):
    value: bool

@dataclass
class VarBool(BoolExp):
    name: str

@dataclass
class And(BoolExp):
    """conjunction of two boolean expressions"""
    left: BoolExp
    right: BoolExp

@dataclass
class Or(BoolExp):
    """disjunction of two boolean expressions"""
    left: BoolExp
    right: BoolExp

@dataclass
class Not(BoolExp):
    """Negation of a boolean expression"""
    value: BoolExp

@dataclass
class Implies(BoolExp):
    """implication of two boolean expressions"""
    left: BoolExp
    right: BoolExp

@dataclass
class ITEInt(IntExp):
    condition: BoolExp
    left: IntExp
    right: IntExp

@dataclass
class ITEBool(BoolExp):
    condition: BoolExp
    left: BoolExp
    right: BoolExp

@dataclass
class Eq(BoolExp):
    left: Exp
    right: Exp

@dataclass
class Neq(BoolExp):
    left: Exp
    right: Exp

@dataclass
class InRange(BoolExp):
    expr: IntExp
    abitype: AbiType
    # only allow (int, uint, address) 

# arithmetic
@dataclass
class LitInt(IntExp):
    value: int

@dataclass
class VarInt(IntExp):
    name: str

@dataclass
class Add(IntExp):
    """addition of two integer expressions"""
    left: IntExp
    right: IntExp

@dataclass 
class Sub(IntExp):
    """subtraction of two integer expressions"""
    left: IntExp
    right: IntExp

@dataclass
class Mul(IntExp):
    """multiplication of two integer expressions"""
    left: IntExp
    right: IntExp

@dataclass
class Div(IntExp):
    """division of two integer expressions"""
    left: IntExp
    right: IntExp

@dataclass
class Pow(IntExp):
    """division of two integer expressions"""
    left: IntExp
    right: IntExp


# relations of IntBool
@dataclass
class Lt(BoolExp):
    """less than comparison of two integer expressions"""
    left: IntExp
    right: IntExp

@dataclass
class Le(BoolExp):
    """less than or equal comparison of two integer expressions"""
    left: IntExp
    right: IntExp

@dataclass
class Gt(BoolExp):
    """greater than comparison of two integer expressions"""
    left: IntExp
    right: IntExp

@dataclass
class Ge(BoolExp):
    """greater than or equal comparison of two integer expressions"""
    left: IntExp
    right: IntExp




    
# --- environment Variables ---

@dataclass  
class EnvVarInt(IntExp):
    """A reference to an environment variable (e.g. msg.sender)"""
    name: str

@dataclass  
class EnvVarBool(BoolExp):
    """A reference to an environment variable (e.g. msg.sender)"""
    name: str

@dataclass    
class StorageItem(Exp): # should it also be either bool or int?
    """This is TItem in TimeAgnostic.hs"""
    loc: StorageLoc
    time: Timing





# --- Storage Location ---

class StorageLoc(metaclass=ABCMeta):
    """A reference to an item in storage"""

@dataclass
class VarLoc(StorageLoc):
    """The base variable reference type
       This can either be a value type, or the base of a longer chain of e.g. MappingLoc / ContractLoc expressions
    """ 
    # the contract in which this storage location resides
    contract: str
    # the name of the storage location
    name: str

@dataclass    
class MappingLoc(StorageLoc):
    """A fully applied lookup in a (potentially nested) mapping
       e.g. m[4][3] 
    """
    # the location in storage that holds the mapping (e.g. the m in m[4][3])
    loc: StorageLoc
    # the arguments to the mapping that give us an actual location in storage (e.g. the [4][3] in m[4][3])
    args: List[Exp]

@dataclass    
class ContractLoc(StorageLoc):
    """A reference to a field on a contract that is held in storage
       e.g. c.x.y[3]
    """
    # the location in storage that holds the pointer to the contract (e.g. the c in c.x)
    loc: StorageLoc
    # the name of the contract that the field belongs to (e.g. the type of c in c.x)
    contract: str
    # the name of the field (e.g. the "x" in c.x)
    field: str


class Timing(metaclass=ABCMeta):
    """Is the storage varaible refering to the pre or post state"""

@dataclass
class Pre(Timing):
    """Prestate"""

@dataclass
class Post(Timing):
    """Poststate"""


act_ast.py
sophierain/contract2game
from typing import Union, Set, Dict, List
from dataclasses import dataclass
from parse_act import *
from act_ast import *
import z3

Integer = Union[int, z3.ArithRef]
Boolean = Union[bool, z3.BoolRef]
SymVar = Union[Integer, Boolean, z3.FuncDeclRef]

# contract -> field name -> z3 variable
SymStore = Dict[str, Dict[str, SymVar]]
# var name -> z3 variable
SymEnv = Dict[str, Integer]
# var name -> z3 variable
SymCalldata = Dict[str, SymVar]

"""
x = z3.Int(<name>)                                              integer constant named <name>
z = z3.Bool(<name>)                                                     boolean constant named <name>
y = z3.Function(<fct_name>, <z3 input sort(s)>, <z3 ouput sort>)   uninterpreted function named <fct_name>

"""

postint = z3.Function("postint", z3.IntSort(), z3.IntSort())
postbool = z3.Function("postbool", z3.BoolSort(), z3.BoolSort())


@dataclass
class SymState:
    storage: SymStore
    constraints: Set[z3.BoolRef]


class BaseTree(metaclass=ABCMeta):
    """base class for game trees"""

@dataclass
class Tree(BaseTree):
    """a non-leaf node with children"""
    state: SymState
    children: Dict[str, BaseTree]



"""Returns the constraints from a behavior that are relevant for the consruction of the game tree"""
def extract_constraints(behv: Behavior) -> Set[BoolExp]:
    return set(behv.caseConditions + behv.preConditions + behv.stateUpdates)

def to_smt(env: SymEnv, calldata: SymCalldata, prestore: SymStore, exp: BoolExp) -> Boolean:
    pass

def apply_behaviour(state: SymState, behv: Behavior) -> SymState:
    pass

def reachable(state: SymState) -> z3.CheckSatResult:
    pass


def init_state(storage: Storage, ctor: Constructor, extraConstraints: Set[BoolExp]) -> SymState:
    """translate storage information to smt concepts, and collect initial constraints from user and invariants"""
    state = dict()
    for key, value in storage.items():
        state[key] = dict()
        for nested_key, nested_value in value.items():
            state[key][nested_key] = slottype2smt(nested_value)
    
    smt_constraints = []
    for exp in extraConstraints:
        smt_constraints.append(generate_smt_constraint(exp), [])
    for exp in ctor.invariants:
        smt_constraints.append(generate_smt_constraint(exp), [])

    return SymState(state, set(smt_constraints))



def generate_tree(tree: Tree, behvs: Set[Behavior]) -> Tree:
    """recursively extends the tree by applying all behaviors to all leaves until no new reachable states are found"""
    pass
    


def slottype2smt(slot: SlotType) -> SymVar:
    pass



def generate_smt_constraint(exp: BoolExp, history: List[str]) -> Boolean:
    """
    LitBool
    VarBool
    EnvVarBool
    ??? StorageItem ???
    And
    Or
    Not
    Implies
    ITEBool
    Eq - KIM StorageItem
    Neq - KIM StorageItem
    InRange
    Lt
    Le
    Gt
    Ge
    """
    if isinstance(exp, LitBool):
        return exp.value
    
    elif isinstance(exp, VarBool):
        label = to_label(history, exp.name)
        return z3.Bool(label)
    
    elif isinstance(exp, EnvVarBool):
        label = to_label(history, exp.name)
        return z3.Bool(label)
    
    # ATTENTION StorageItem not a BoolExp nor an IntExp
    # Question: What can be done with StorageItem? only assigning new values?

    # elif isinstance(exp, StorageItem):
    #     
    #     result = generate_smt_storageloc(exp.loc, history)
    #     if isinstance(exp.time, Post):
    #         return postbool(result)
    #     else:
    #         return result
    
    elif isinstance(exp, And):
        return z3.And(generate_smt_constraint(exp.left, history),
                      generate_smt_constraint(exp.right, history)
                      )
    
    elif isinstance(exp, Or):
        return z3.Or(generate_smt_constraint(exp.left, history), 
                     generate_smt_constraint(exp.right, history)
                     )
    
    elif isinstance(exp, Not):
        return z3.Not(generate_smt_constraint(exp.value, history))
    
    elif isinstance(exp, Implies):
        return z3.Implies(generate_smt_constraint(exp.left, history), 
                          generate_smt_constraint(exp.right, history)
                          )
    
    elif isinstance(exp, ITEBool):
        return z3.And(z3.Implies(
                            generate_smt_constraint(exp.condition, history), 
                            generate_smt_constraint(exp.left, history)),
                      z3.Implies(
                            z3.Not(generate_smt_constraint(exp.condition, history)),
                            generate_smt_constraint(exp.right, history))
                            )
    
    elif isinstance(exp, Eq):
        # KIM: StorageItem
        if isinstance(exp.left, BoolExp) and isinstance(exp.right, BoolExp):
            return generate_smt_constraint(exp.left, history) == generate_smt_constraint(exp.right, history)
        elif isinstance(exp.left, IntExp) and isinstance(exp.right, IntExp):
            return generate_smt_term(exp.left, history) == generate_smt_term(exp.right, history)
        else:
            assert False, "left and right have to be of the same type"

    elif isinstance(exp, Neq):
        # KIM StorageItem
        if isinstance(exp.left, BoolExp) and isinstance(exp.right, BoolExp):
            return z3.Not(
                          generate_smt_constraint(exp.left, history) == generate_smt_constraint(exp.right, history)
                          )
        elif isinstance(exp.left, IntExp) and isinstance(exp.right, IntExp):
            return z3.Not(
                            generate_smt_term(exp.left, history) == generate_smt_term(exp.right, history)
                            )
        else:
            assert False, "left and right have to be of the same type"

    elif isinstance(exp, InRange):
        if isinstance(InRange.abitype, AbiIntType):
            min = -2**(InRange.abitype.size -1)
            max = 2**(InRange.abitype.size -1) -1
        elif isinstance(InRange.abitype, AbiUIntType):
            min = 0
            max = (2**InRange.abitype.size) -1
        elif isinstance(InRange.abitype, AbiAddressType):
            min = 0
            max = (2**256) -1
        else:
            assert False, "unsupported abitype for inrange"
        return z3.And(
                    generate_smt_constraint(Le(min, exp.expr), history),
                    generate_smt_constraint(Le(exp.expr, max), history)
                    )
    
    elif isinstance(exp, Lt):
        return generate_smt_constraint(exp.left, history) < generate_smt_constraint(exp.right, history)

    elif isinstance(exp, Le):
        return generate_smt_constraint(exp.left, history) <= generate_smt_constraint(exp.right, history)
    
    elif isinstance(exp, Gt):
        return generate_smt_constraint(exp.left, history) > generate_smt_constraint(exp.right, history)
    
    else:
        assert isinstance(exp, Ge)
        return generate_smt_constraint(exp.left, history) >= generate_smt_constraint(exp.right, history)





def generate_smt_term(exp: IntExp, history: List[str]) -> Integer:
    """
    LitInt
    VarInt
    EnvVarInt
    ??? StorageItem ???
    Add
    Sub
    Mul
    Div
    Pow 
    ??? ITEInt ???
    """

    if isinstance(exp, LitInt):
        return exp.value
    
    elif isinstance(exp, VarInt):
        return z3.Int(to_label(history, exp.name))
    
    elif isinstance(exp, EnvVarInt):
        return z3.Int(to_label(history, exp.name))
    
    # ATTENTION StorageItem not a BoolExp nor an IntExp
    # Question: What can be done with StorageItem? only assigning new values?

    # elif isinstance(exp, StorageItem):
    #     
    #     result = generate_smt_storageloc(exp.loc, history)
    #     if isinstance(exp.time, Post):
    #         return postint(result)
    #     else:
    #         return result

    elif isinstance(exp, Add):
        return generate_smt_term(exp.left, history) + generate_smt_term(exp.right, history)
    
    elif isinstance(exp, Sub):
        return generate_smt_term(exp.left, history) - generate_smt_term(exp.right, history)
    
    elif isinstance(exp, Mul):
        return generate_smt_term(exp.left, history) * generate_smt_term(exp.right, history)
    
    elif isinstance(exp, Div):
        return generate_smt_term(exp.left, history) / generate_smt_term(exp.right, history)
    
    elif isinstance(exp, Pow):
        left = generate_smt_term(exp.left, history)
        right = generate_smt_term(exp.right, history)
        assert isinstance(left, int) & isinstance(right, int), "symbolic exponentiation not supported"
        return left ** right

    else:
        # I am pretty sure that this is not correct SMT code:
        # x(6) == (if b then 8 else 20)
        # should rather be 
        # (b => x(6) == 8) and (not b => x(6) == 20)
        assert isinstance(exp, ITEInt)
        return z3.And(z3.Implies(
                            generate_smt_constraint(exp.condition, history), 
                            generate_smt_term(exp.left, history)),
                    z3.Implies(
                            z3.Not(generate_smt_constraint(exp.condition, history)),
                            generate_smt_term(exp.right, history)))
        



def to_label(history: List[str], name: str) -> str:
    label = ""

    for elem in history:
        label = label + ";" + elem

    label = label + ";" + name
    return label



def from_label(label: str) -> (List[str], str):

    res = label.split(";")
    assert len(res)>0

    return res[:-1], res[-1]

"""
contract C {
  uint x;
  uint y;
  bool z;

  function(uint i, uint j) {
  
  }
}


"C": {
    x: AbiUintType(256),
    y: AbiUintType(256),
    z: AbiBoolType
}

---

"C": {
    x: z3.IntRef,
    y: z3.IntRef,
    z: z3.BoolRef
}

0 <= x <= 2^256
0 <= y <= 2^256

"""



# @dataclass
# class SMT_Behavior:
#     name: str
#     caseConditions: Boolean
#     preConditions: Boolean
#     postConditions: Boolean
#     stateUpdates: Boolean

# @dataclass
# class SMT_Contract:
#     name: str
#     behaviors: List[SMT_Behavior]

# def act_to_smt(act: Act) -> List[SMT_Contract]:
#     return [contract_to_smt(elem, act["store"]) for elem in act["contracts"]]

# def contract_to_smt(contract: Contract, store: Storage) -> SMT_Contract:
#     return SMT_Contract(contract["name"], [behavior_to_smt(elem, contract["constructor"], store) for elem in contract["behaviors"]])

# def behavior_to_smt(behv: Behavior, contr: Constructor, store: Storage) -> SMT_Behavior:

#     case = conjunction(*[generate_constraint(elem, contr, store) for elem in behv["caseConditions"]])
#     pre = conjunction(*[generate_constraint(elem, contr, store) for elem in behv["preConditions"]])
#     post = conjunction(*[generate_constraint(elem, contr, store) for elem in behv["postConditions"]])
#     updates = conjunction(*[generate_constraint(elem, contr, store) for elem in behv["stateUpdates"]])

#     return SMT_Behavior(behv["name"], case, pre, post, updates)

# def generate_constraint(boolexp: BoolExp, contr: Constructor, store: Storage) -> Boolean:
#     # are Contructor and Storage needed for our purpose?
    
#     if isinstance(boolexp, LitBool):
#         return boolexp["value"]
#     elif isinstance(boolexp, VarBool):
#         return z3.Bool(boolexp["name"])
    


ast2smt.py
sophierain/contract2game
# allow type annotations for the current class
# minimum version: 3.7, will be default in future
from __future__ import annotations

from typing import Callable, Optional, Union, Set, Generator, Tuple
from fractions import Fraction
import z3

Real = Union[float, z3.ArithRef]
Boolean = Union[bool, z3.BoolRef]
LabelFn = Optional[Callable[[Real, Real, Boolean, bool], Optional[z3.BoolRef]]]


def negation(to_negate: Boolean) -> z3.BoolRef:
    """negate a Z3 expression while satisfying the type checker"""
    negated = z3.Not(to_negate)
    assert isinstance(negated, z3.BoolRef)
    return negated


def disjunction(*disjuncts: Boolean) -> z3.BoolRef:
    """build a Z3 disjunction while satisfying the type checker"""
    result = z3.Or(disjuncts)
    assert isinstance(result, z3.BoolRef)
    return result


def conjunction(*conjuncts: Boolean) -> z3.BoolRef:
    """build a Z3 conjunction while satisfying the type checker"""
    result = z3.And(conjuncts)
    assert isinstance(result, z3.BoolRef)
    return result


def implication(left: Boolean, right: Boolean) -> z3.BoolRef:
    """build a Z3 implication while satisfying the type checker"""
    return z3.Implies(left, right)


def simplify_boolean(expr: z3.BoolRef) -> z3.BoolRef:
    """simplify the Boolean `expr` while satisfying the type checker"""
    simplified = z3.simplify(expr)
    assert isinstance(simplified, z3.BoolRef)
    return simplified


def label(
        left: Real,
        right: Real,
        op: Callable[[Real, Real], Boolean],
        label_fn: LabelFn,
        real: bool
) -> Boolean:
    """
    build the expression `(label => op(left, right))`

    `label_fn(left, right, real)` is called to supply `label`
    """
    comparison = op(left, right)
    if label_fn is None:
        return comparison
    label_expr = label_fn(left, right, comparison, real)
    if label_expr is None:
        return comparison

    return implication(label_expr, comparison)


def valuation(term: Real, model: z3.ModelRef) -> Fraction:
    """Evaluate the term according to the model"""
    if not isinstance(term, z3.ArithRef):
        return Fraction(term)

    value = model.evaluate(term, model_completion=True)
    assert isinstance(value, z3.RatNumRef) or isinstance(value, z3.IntNumRef)
    value = value.as_fraction() if isinstance(value, z3.RatNumRef) else Fraction(value.as_long())
    return value


def order_according_to_model(model: z3.ModelRef, minimize: z3.Solver, terms: Set[Tuple[Real, Real]]) -> Set[Boolean]:
    """
    compute the order of terms according to the model and return it as a set of constraints
    (also exclude those that can be shown by `minimize`)
    """

    def split(left: Real, right: Real) -> Boolean:
        left_val = valuation(left, model)
        right_val = valuation(right, model)
        if left_val > right_val:
            return left > right
        elif left_val == right_val:
            return left == right
        else:
            return left < right

    comparisons = {
        split(left, right)
        for left, right in terms
    }

    redundant = set()
    for comparison in comparisons:
        if minimize.check(*(comparisons - redundant - {comparison}), negation(comparison)) == z3.unsat:
            redundant.add(comparison)

    return comparisons - redundant


# following functions adapted from "Programming Z3"
def maximal_satisfying_subset(solver: z3.Solver,
                              start: Set[z3.BoolRef],
                              all_labels: Set[z3.BoolRef],
                              *assumptions: z3.BoolRef) -> Set[z3.BoolRef]:
    """compute a maximal satisfying subset of `all`, starting from `start` with respect to `solver` + `assumptions`"""
    ps = all_labels - start
    mss = start
    backbones = set()
    while len(ps) > 0:
        p = ps.pop()
        if solver.check(*(mss | backbones | {p}), *assumptions) == z3.sat:
            model = solver.model()
            mss = mss | {p} | {
                q for q in ps
                if z3.is_true(model.eval(q))
            }
            ps = ps - mss
        else:
            backbones = backbones | {negation(p)}

    return mss


def minimal_unsat_cores(solver: z3.Solver, all_labels: Set[z3.BoolRef], *assumptions: z3.BoolRef) -> \
        Generator[Set[z3.BoolRef], None, None]:
    """iteratively compute all minimal unsat cores in `all` with respect to `solver` + `assumptions`"""
    solver.set("core.minimize", True)
    map_solver = z3.Solver()
    map_solver.set("unsat_core", True)
    map_solver.set("core.minimize", True)
    while map_solver.check() == z3.sat:
        model = map_solver.model()
        seed = {
            p for p in all_labels
            if not z3.is_false(model.eval(p))
        }
        if solver.check(*seed, *assumptions) == z3.sat:
            mss = maximal_satisfying_subset(solver, seed, all_labels, *assumptions)
            map_solver.add(disjunction(*(all_labels - mss)))
        else:
            mus = {
                label_expr
                for label_expr in solver.unsat_core()
                if isinstance(label_expr, z3.BoolRef) and label_expr in all_labels
            }
            map_solver.add(disjunction(*(negation(label_expr) for label_expr in mus)))
            yield mus

auxfunz3.py
sophierain/contract2game
from enum import Enum
import z3

class SecurityProperty(Enum):
    WEAK_IMMUNITY = 'wi'
    WEAKER_IMMUNITY = 'weri'
    COLLUSION_RESILIENCE = 'cr'
    PRACTICALITY = 'pr'


PROPERTY_TO_STR = {SecurityProperty.WEAK_IMMUNITY: 'weak immunity',
                   SecurityProperty.WEAKER_IMMUNITY: 'weaker immunity',
                   SecurityProperty.COLLUSION_RESILIENCE: 'collusion resilience',
                   SecurityProperty.PRACTICALITY: 'practicality'}

PROPERTY_TO_JSON_KEY = {SecurityProperty.WEAK_IMMUNITY: 'weak_immunity',
                        SecurityProperty.WEAKER_IMMUNITY: 'weaker_immunity',
                        SecurityProperty.COLLUSION_RESILIENCE: 'collusion_resilience',
                        SecurityProperty.PRACTICALITY: 'practicality'}
ANALYSIS_JSON_KEY = "analysis"
HONEST_HISTORY_JSON_KEY = "honest_history"
JOINT_STRATEGIES_JSON_KEY = "joint_strategies"
GENERATED_PRECONDITIONS_JSON_KEY = "generated_preconditions"
COUNTEREXAMPLES_JSON_KEY = "counterexamples"
COUNTEREXAMPLE_ORDERING_JSON_KEY = "ordering"
COUNTEREXAMPLE_STRATEGIES_JSON_KEY = "strategies"
COUNTEREXAMPLE_HISTORIES_JSON_KEY = "histories"
JOINT_STRATEGY_ORDERING_JSON_KEY = "ordering"
JOINT_STRATEGY_STRATEGY_JSON_KEY = "strategy"

CONSTRAINT_FUNS = {
    'Or': z3.Or,
    'And': z3.And,
    'Not': z3.Not
}

constants.py
sophierain/contract2game
from act_ast import *
from typing import Dict, List

def parse_act_json(obj: Dict) -> Act:
    # assert 'store' in obj, "message"
    assert obj["kind"]=="Program", "'kind' key does not match 'Program'"
    assert "store" in obj, "Missing 'store' key"
    assert "contracts" in obj, "Missing 'contracts' key"

    return Act(parse_store(obj["store"]), [parse_contract(elem) for elem in obj["contracts"]])


def parse_store(store: Dict) -> Storage:
    
    assert store["kind"]=="Storages", "'kind' key does not match 'Storages'"
    assert "storages" in store, "Missing 'storages' key"

    store_dict: Dict[str, Dict] = dict()

    for key, value in store.items():
        store_dict[key] = dict()
        for nested_key, nested_value in value.items():
            store_dict[key][nested_key] = parse_slottype(nested_value)

    return Storage(store_dict) 

def parse_slottype(input: List) -> SlotType:

    assert len(input)==2, "incorrect storage variable format"

    slottype = input[0]
    assert "kind" in slottype, "Missing 'kind' key"

    if slottype["kind"] == "ValueType":
        assert "valueType" in slottype, "Missing 'valueType' key"
        return parse_valuetype(slottype["valueType"])

    elif slottype["kind"] == "MappingType":
        assert "ixTypes" in slottype, "Missing 'ixTypes' key"
        assert "resType" in slottype, "Missing 'resType' key"
        return MappingType([parse_valuetype(elem) for elem in slottype["ixTypes"]], parse_valuetype(slottype["restype"]))
    
    else:
        assert False, "Unsupported slottype: " + slottype["kind"] 
        
def parse_valuetype(valuetype: Dict) -> ValueType:
    assert "kind" in valuetype,"Missing 'kind' key"

    if valuetype["kind"]== "ContractType":
        assert "name" in valuetype, "missing 'name' key"
        return ContractType(valuetype["name"])
    
    elif valuetype["kind"] == "AbiType":
        assert "abiType" in valuetype, "Missing 'abiType' key" 
        return parse_abitype(valuetype["abiType"])
    
    else:
        assert False, "Unsupported value type: " + valuetype["kind"]

def parse_abitype(abi: Dict) -> AbiType:
    assert "type" in abi, "Missing 'type' key"

    if abi["type"]== "UInt":
        assert "size" in abi, "Missing 'size' key"
        return AbiUIntType(int(abi["size"]))
    elif abi["type"]== "Int":
        assert "size" in abi, "Missing 'size' key"
        return AbiIntType(int(abi["size"]))
    elif abi["type"]== "Address":
        return AbiAddressType()
    elif abi["type"]== "Bool":
        return AbiBoolType()
    elif abi["type"]== "Bytes":
        assert "size" in abi, "Missing 'size' key"
        return AbiBytesType(int(abi["size"]))
    elif abi["type"]== "BytesDynamic":
        return AbiBytesDynamicType() 
    elif abi["type"]== "String":
        return AbiStringType() 
    elif abi["type"]== "ArrayDynamic":
        assert "arraytype" in abi, "Missing 'arraytype' key"
        return AbiArrayDynamicType(parse_abitype(abi["arraytype"]))
    elif abi["type"]== "Array":
        assert "size" in abi, "Missing 'size' key"
        assert "arraytype" in abi, "Missing 'arraytype' key"
        return AbiArrayType(int(abi["size"]), parse_abitype(abi["arraytype"]))
    elif abi["type"]== "Tuple":
        assert "elemTypes" in abi, "Missing 'elemTypes' key"
        return AbiTupleType([parse_abitype(elem) for elem in abi["elemTypes"]])
    elif abi["type"]== "Function":
        return AbiFunctionType()
    else:
        assert False, "Unsupported abi type: " + abi["type"]
    
    

def parse_contract(contract: Dict) -> Contract:
    
    assert contract["kind"]=="Contract", "'kind' key does not match 'Contract'"
    assert "constructor" in contract, "Missing 'constructor' key"
    assert "behaviors" in contract, "Missing 'behaviors' key"
    assert "contract" in contract["constructor"], "Missing 'contract' key at 'contract['constructor']'"

    return Contract(contract["constructor"]["contract"], parse_constructor(contract["constructor"]), [parse_behavior(elem) for elem in contract["behaviors"]])



def parse_constructor(ctor: Dict)-> Constructor:
    
    assert ctor["kind"]=="Constructor", "'kind' key does not match 'Constructor'"
    assert "initial_storage" in ctor, "Missing 'initial_storage' key"
    assert "interface" in ctor, "Missing 'interface' key"
    assert "invariants" in ctor, "Missing 'invariants' key"
    assert "preConditions" in ctor, "Missing 'preConditions' key"
    assert "postConditions" in ctor, "Missing 'postConditions' key"

    return Constructor(
                        parse_interface(ctor["interface"]),
                        [parse_boolexp(elem) for elem in ctor["initial_storage"] ],
                        [parse_boolexp(elem) for elem in ctor["preConditions"] ],
                        [parse_boolexp(elem) for elem in ctor["postConditions"] ],
                        [parse_boolexp(elem) for elem in ctor["invariants"] ]
                        )

def parse_behavior(behv: Dict) -> Behavior:
    # kind Behaviour
    assert behv["kind"]=="Behaviour", "'kind' key does not match 'Behaviour'"
    assert "name" in behv, "Missing 'name' key"
    assert "interface" in behv, "Missing 'interface' key"
    assert "case" in behv, "Missing 'case' key"
    assert "preConditions" in behv, "Missing 'preConditions' key"
    assert "postConditions" in behv, "Missing 'postConditions' key"
    assert "returns" in behv, "Missing 'returns' key"
    assert "stateUpdates" in behv, "Missing 'stateUpdates' key"


    return Behavior(
                    behv["name"],
                    parse_interface(behv["interface"]),
                    [parse_boolexp(elem) for elem in behv["case"] ],
                    [parse_boolexp(elem) for elem in behv["preConditions"] ],
                    [parse_boolexp(elem) for elem in behv["postConditions"] ],
                    parse_exp(behv["returns"]),
                    [parse_stateupdate(elem) for elem in behv["stateUpdates"] ]
                    )

def parse_interface(interface: Dict) -> Interface:
    assert "kind" in interface, "Missing 'kind' key"
    assert interface["kind"]=="Interface", "Unexpected 'kind': " + interface["kind"]+", expected 'Interface'"
    assert "id" in interface, "Missing 'id' key"
    assert "args" in interface, "Missing 'args' key"
    return Interface(interface["id"], [parse_decl(elem) for elem in interface["args"]])
                     
def parse_decl(decl: Dict) -> Decl:
    assert "kind" in decl, "Missing 'kind' key"
    assert decl["kind"]=="Declaration", "Unexpected 'kind': " + decl["kind"]+", expected 'Declaration'"
    assert "id" in decl, "Missing 'id' key"
    assert "abitype" in decl, "Missing 'abitype' key"
    return Decl(decl["id"], parse_abitype(decl["abitype"])) 

# the following code expects all input to be dicts
# either a base case dict:
#   "literal": "x",
#   "type": 'int"
# or another base case dict:
#   "var": "x",
#   "type": "bool"
# or yet another base case dict:
#   "envValue": "x",
#   "type": "int" or "bool"
# or  for storageitems:
#   "entry": Dict,
#   "timing": "Pre" or "Post"
#
# or recursive case containing
#           "symbol": "<=",
#           "args": [...],
#           "type": "int"



def parse_boolexp(boolexp: Dict) -> BoolExp:
    res = parse_exp(boolexp)
    assert type(res)==BoolExp, "not a boolean expression"
    return res

def parse_intexp(intexp: Dict) -> IntExp:
    res = parse_exp(intexp)
    assert type(res)==IntExp, "not an integer expression"
    return res

def parse_typedexp(texp: Dict) -> Exp:

    assert "type" in texp, "Missing 'type' key"    
    assert "expression" in texp, "Missing 'expression' key"
    
    if texp["type"] == "AInteger":
        return parse_intexp(texp["expression"])
    elif texp["type"] == "ABoolean":
        return parse_boolexp(texp["expression"])
    else:
        assert False, "Unsupported type: " + texp["type"]


def parse_exp(exp: Dict) -> Exp:

    keys = exp.keys()
    if "symbol" in keys:
        #recursive case
        assert "type" in keys, "Missing 'type' key"    
        assert "args" in keys, "Missing 'args' key"

        return parse_symbol(exp["symbol"], exp["type"], [parse_exp(elem) for elem in exp["args"]])

    else:
        # Base Case
        if "literal" in keys:
            # Literal; either int or bool
            assert "type" in keys, "Missing 'type' key" 
            if exp["type"] == "int":
                return LitInt(int(exp["literal"]))
            elif exp["type"] == "bool":
                return LitBool(bool(exp["literal"]))
            else:
                assert False, "unsupported literal type"

        elif "var" in keys:
            # Variable; either int or bool
            assert "type" in keys, "Missing 'type' key"
            if exp["type"] == "int":
                return VarInt(exp["var"])
            elif exp["type"] == "bool":
                return VarBool(exp["var"])
            else:
                assert False, "unsupported variable type"
    
        elif "envValue" in keys:
            # environment value; either int or bool
            assert "type" in keys, "Missing 'type' key" 
            if exp["type"] == "int":
                return EnvVarInt(exp["envValue"])
            elif exp["type"] == "bool":
                return EnvVarBool(exp["envValue"])
            else:
                assert False, "unsupported environment variable type"

        elif "entry" in keys:
            # storage item; with timing either pre or post
            assert "timing" in keys, "Missing 'type' key"
            if exp["timing"] == "Pre":
                return StorageItem(parse_storageloc(exp["entry"]), Pre())
            elif exp["timing"] == "Post":
               return StorageItem(parse_storageloc(exp["entry"]), Post())
            else:
                assert False, "unsupported timing value" 

        else:
            assert False, "unknown expression"


def parse_storageloc(sloc: Dict) -> StorageLoc:

    assert "kind" in sloc, "Missing 'kind' key"

    if sloc["kind"] == "Mapping":
        assert "reference" in sloc, "Missing 'reference' key"
        assert "indexes" in sloc, "Missing 'indexes' key"
        return MappingLoc(parse_storageloc(sloc["reference"]), [parse_exp(elem) for elem in sloc["indexes"]])

    elif sloc["kind"] == "SVar":
        # VarLoc case:
        assert "svar" in sloc, "Missing 'svar' key"
        assert "contract" in sloc, "Missing 'contract' key"
        return VarLoc(sloc["contract"], sloc["svar"])

    elif sloc["kind"] == "Field": 
        # ContractLoc case:
        assert "reference" in sloc, "Missing 'reference' key"
        assert "field" in sloc, "Missing 'field' key"
        assert "contract"in sloc, "Missing 'contract' key"
        return ContractLoc(sloc["reference"] , sloc["contract"], sloc["field"])
    
    else:
        assert False, "unsupported storage kind: " + sloc["kind"]

def parse_symbol(symbol: str, type: str, args: List)-> Exp:    

        if symbol == "+":
            assert  len(args) == 2, "two arguments expected for +"
            assert all(isinstance(elem, IntExp) for elem in args), "expected integer expression arguments" 
            return Add(*args)
        elif symbol == "-":
            assert len(args) == 2, "two arguments expected for -"
            assert all(isinstance(elem, IntExp) for elem in args), "expected integer expression arguments" 
            return Sub(*args)
        elif symbol == "*":
            assert len(args) == 2, "two arguments expected for *"
            assert all(isinstance(elem, IntExp) for elem in args), "expected integer expression arguments" 
            return Mul(*args)
        elif symbol == "/":
            assert len(args) == 2, "two arguments expected for /"
            assert all(isinstance(elem, IntExp) for elem in args), "expected integer expression arguments" 
            return Div(*args)
        elif symbol == "^":
            assert len(args) == 2, "two arguments expected for ^"
            assert all(isinstance(elem, IntExp) for elem in args), "expected integer expression arguments" 
            return Pow(*args)


        elif symbol == "inrange": 
            assert len(args) == 2, "two arguments expected for 'inrange'"
            assert isinstance(args[0],IntExp), "first argument expected to be an integer expression"
            assert isinstance(args[1],AbiIntType) or isinstance(args[1],AbiUIntType) or isinstance(args[1],AbiAddressType), \
                   "second argument expected to be of abi type int, uint or address"
            return InRange(*args)
       

        elif symbol == "ite":
            assert len(args) == 3, "three arguments expected for 'ite'"
            if type=="int":
                assert isinstance(args[0],BoolExp),"expected boolean expression arguments"
                assert all(isinstance(elem, IntExp) for elem in args[1:]), "expected integer expression arguments" 
                return ITEInt(*args)
            elif type == "bool":
                assert all(isinstance(elem, BoolExp) for elem in args), "expected boolean expression arguments" 
                return ITEBool(*args)
            else:
                assert False, "Unsupported 'ite' type: " +type
        elif symbol == "=/=":
            assert len(args) == 2, "two arguments expected for '=/='"
            all_bool = all(isinstance(elem, BoolExp) for elem in args)
            all_int = all(isinstance(elem, IntExp) for elem in args)
            assert all_bool or all_int, "expected all boolean or all integer expression arguments" 
            return Neq(*args)
        elif symbol == "==":
            assert len(args) == 2, "two arguments expected for '=='"
            all_bool = all(isinstance(elem, BoolExp) for elem in args)
            all_int = all(isinstance(elem, IntExp) for elem in args)
            assert all_bool or all_int, "expected all boolean or all integer expression arguments" 
            return Eq(*args)

        elif symbol == "and":
            assert len(args) == 2, "two arguments expected for 'and'"
            assert all(isinstance(elem, BoolExp) for elem in args), "expected boolean expression arguments" 
            return And(*args)
        elif symbol == "or":
            assert len(args) == 2, "two arguments expected for 'or'"
            assert all(isinstance(elem, BoolExp) for elem in args), "expected boolean expression arguments" 
            return Or(*args)
        elif symbol == "not":
            assert len(args) == 1, "one argument expected for 'not'"
            assert all(isinstance(elem, BoolExp) for elem in args), "expected boolean expression arguments" 
            return Not(*args)
        elif symbol == "=>":
            assert len(args) == 2, "two arguments expected for '=>'"
            assert all(isinstance(elem, BoolExp) for elem in args), "expected boolean expression arguments" 
            return Implies(*args)

        elif symbol == "<":
            assert len(args) == 2, "two arguments expected for '<'"
            assert all(isinstance(elem, IntExp) for elem in args), "expected integer expression arguments" 
            return Lt(*args)
        elif symbol == ">":
            assert len(args) == 2, "two arguments expected for '>'"
            assert all(isinstance(elem, IntExp) for elem in args), "expected integer expression arguments" 
            return Gt(*args)
        elif symbol == "<=":
            assert len(args) == 2, "two arguments expected for '<='"
            assert all(isinstance(elem, IntExp) for elem in args), "expected integer expression arguments" 
            return Le(*args)
        elif symbol == ">=":
            assert len(args) == 2, "two arguments expected for '>='"
            assert all(isinstance(elem, IntExp) for elem in args), "expected integer expression arguments" 
            return Ge(*args)
        else:
            assert False, "Unsupported symbol: " + symbol

# remove constant 'blocks' from json, 
# rewrites are thus the only remaining stateupdates and hence the word rewrite can go away
# expect:
#   "location": StorageLocation
#   "value": Expression
# build an equality constraint:
#   post of location = value
# hence this is storageItem with loc=location

def parse_stateupdate(update: Dict) -> BoolExp:

    assert "location" in update, "Missing 'location' key"    
    assert "value" in update, "Missing 'value' key"    
    return Eq(
        StorageItem(
            parse_storageloc(update["location"]), 
            Post()
        ), 
        parse_exp(update["value"])
    )


parse_act.py
sophierain/contract2game
from __future__ import annotations

from abc import ABCMeta, abstractmethod
from dataclasses import dataclass
import itertools
import json

from typing import Any, Dict, Iterable, List, Union
import z3
from auxfunz3 import Boolean
from constants import CONSTRAINT_FUNS
from utility import Utility


#the directly to z3 code:

def load_smtconstraint(source: Union(dict, str))-> Union(Boolean, Utility):
        if isinstance(source, str):
            return Utility.from_name(source, True)

        else:
            list_of_expressions = []
            print(source)
            if "args" in source.keys():
                for expr in source["args"]:#how does the pre thing work there
                    list_of_expressions.append(load_smtconstraint(expr))

                return apply_smtsymbol(list_of_expressions, source["symbol"])
            elif "Pre" in source.keys():
                return load_smtconstraint(source["Pre"]["item"])
            elif "Post" in source.keys():
                return load_smtconstraint(source["Post"]["item"])

def apply_smtsymbol(list_of_expressions: List, symbol: str)-> Union(Boolean, Utility):
        if symbol == "+":
            return list_of_expressions[0] + list_of_expressions[1]
        elif symbol == "-":
            return list_of_expressions[0] - list_of_expressions[1]
        elif symbol == "*":
            return list_of_expressions[0] * list_of_expressions[1] #ignores double infinitesimals
        elif symbol == "/":
            return list_of_expressions[0] / list_of_expressions[1] #ignores double infinitesimals
        elif symbol == "^":
            return list_of_expressions[0] ** list_of_expressions[1] #ignores double infinitesimals, only real exponents allowed

        # elif symbol == "litint":
        #     return list_of_expressions[0] 
        # elif symbol == "intmin": 
        #     return -2 ** (list_of_expressions[0] -1)
        # elif symbol == "intmax":
        #     return 2 ** (list_of_expressions[0] -1) -1
        # elif symbol == "uintmin":
        #     return 0
        # elif symbol == "uintmax":
        #     return 2 ** list_of_expressions[0] -1
        elif symbol == "inrange": #arity 2; type and value
            pass #format issue if expression is not a variable of numeric value
        # elif symbol == "intenv":
        #     pass 
        elif symbol == "ite":
            to_be_conjoint = tuple(z3.Implies(list_of_expressions[0],list_of_expressions[1]), z3.Implies(z3.Not(list_of_expressions[0]),list_of_expressions[2]))
            return z3.And(*to_be_conjoint)


        elif symbol == "and":
            return z3.And(*list_of_expressions)
        elif symbol == "or":
            return z3.Or(*list_of_expressions)
        elif symbol == "<":
            return list_of_expressions[0] < list_of_expressions[1]
        elif symbol == ">":
            return list_of_expressions[0] > list_of_expressions[1]
        elif symbol == "=>":
            return z3.Implies(list_of_expressions[0],list_of_expressions[1])
        elif symbol == "=/=":
            return z3.Not(list_of_expressions[0]==list_of_expressions[1])
        elif symbol == "==":
            return list_of_expressions[0]==list_of_expressions[1]
        elif symbol == "<=":
            return list_of_expressions[0] <= list_of_expressions[1]
        elif symbol == ">=":
            return list_of_expressions[0] >= list_of_expressions[1]
        # elif symbol == "LitBool": #???
        #     pass
        elif symbol == "not":
            return z3.Not(list_of_expressions[0])




class SMTBehavior:
    """one function within a contract in a given case"""
    name: str
    case: List[Boolean]
    preConditions: List[Boolean]
    postConditions: List[Boolean]
    returnValue: Union(Boolean, z3.Int) #z3 expression, to be parsed similar to constraints
    stateUpdates: List[Boolean] #equality constraints e.g. update

    def __init__(self, behavior: Dict[str, Any]):
        #assert(behavior["kind"]=="Behavior")
        self.name = behavior["name"]
        self.case = [
            load_smtconstraint(elem) 
            for elem in behavior["case"]
        ]
        self.preConditions = [
            load_smtconstraint(elem) 
            for elem in behavior["preConditions"]
        ]
        self.postConditions = [
            load_smtconstraint(elem)
            for elem in behavior["postConditions"]
        ]
        
        self.returnValue = load_smtconstraint(behavior["returns"]["expression"])
        self.returnType = eval(behavior["returns"]["sort"])
        

        self.stateUpdates = [self.load_smtupdate(elem) for elem in behavior["stateUpdates"]]

    def __repr__(self) -> str:
        return (
            f"name: {self.name}\n"
            f"case: {self.case}\n"
            f"preConditions: {self.preConditions}\n"
            f"postConditions: {self.postConditions}\n"
            f"returnValue: {self.returnValue}\n"
            f"returnType: {self.returnType}\n"
            f"stateUpdates: {self.stateUpdates}\n"
        )

    def load_smtupdate(self, update: Dict) -> Any:
        pass




class SMTConstructor:
    initial_storage: List[Any]
    invariants: List[Boolean] 
    preConditions: List[Boolean]
    postConditions: List[Boolean]

    def __init__(self, constructor: Dict[str, Any]):
        assert(constructor["kind"]=="Constructor")
        self.initial_storage = constructor["initial storage"]
        self.invariants = [
            load_smtconstraint(constraint)
            for constraint in constructor["invariants"]
        ]
        self.preConditions = [
            load_smtconstraint(constraint)
            for constraint in constructor["preConditions"]
        ]        
        self.postConditions = [
            load_smtconstraint(constraint)
            for constraint in constructor["postConditions"]
        ]

    def __repr__(self) -> str:
        return (
            f"initial_storage: {self.initial_storage}\n"
            f"invariants: {self.invariants}\n"
            f"preConditions: {self.preConditions}\n"
            f"postConditions: {self.postConditions}\n"
        )



class SMTContract:
    """input data"""
    behaviors: List[SMTBehavior]
    constructor: SMTConstructor

    def __init__(self, contract: Dict[str, Any]):
        assert(contract["kind"]=="Contract")
        self.constructor = SMTConstructor(contract["constructor"])
        self.behaviors = [SMTBehavior(elem) for elem in contract["behaviors"]]

    def __repr__(self) -> str:
        return (
            f"behaviors:\n {self.behaviors}\n" 
            f"constructor:\n {self.constructor}\n"
        )

parse_act_to_smt.py
sophierain/contract2game
# allow type annotations for the current class
# minimum version: 3.7, will be default in future
from __future__ import annotations

from typing import Callable, Union
import z3
import operator
from auxfunz3 import Real, Boolean, LabelFn, negation, conjunction, disjunction, label


def flip(op: Callable[[Real, Real], Real]) -> Callable[[Real, Real], Real]:
    return lambda x, y: op(y, x)


def add(left: Real, right: Real) -> Real:
    """
    return left + right, except if either is 0
    """
    if type(left) == float and left == 0:
        return right
    elif type(right) == float and right == 0:
        return left
    else:
        return left + right


def sub(left: Real, right: Real) -> Real:
    """
    return left - right, except if either is 0
    """
    if type(left) == float and left == 0:
        return -right
    elif type(right) == float and right == 0:
        return left
    else:
        return left - right


def mul(left: Real, right: Real) -> Real:
    """
    return left * right, except if either is 1
    """
    if type(left) == float and left == 1:
        return right
    elif type(right) == float and right == 1:
        return left
    elif type(right) == float and right == 0:
        return 0
    elif type(left) == float and left == 0:
        return 0
    else:
        result = left * right
        # satisfy linter for some reason
        assert isinstance(result, float) or isinstance(result, z3.ArithRef)
        return result

def div(left: Real, right: Real) -> Real:
    """
    return left / right, except if right is 1
    """

    if type(right) == float and right == 1:
        return left
    else:
        result = left / right
        # satisfy linter for some reason
        assert isinstance(result, float) or isinstance(result, z3.ArithRef)
        return result


class Utility:
    """
    a (real, infinitesimal) pair

    mostly just an adapter pattern for parsing via `eval()`
    and generating Z3 expressions by operator overloading
    """
    real: Real
    inf: Real

    def __init__(self, real: Real, inf: Real):
        """construct from real and infinitesimal parts"""
        self.real = real
        self.inf = inf

    @staticmethod
    def from_real(value: Real) -> Utility:
        """convert a numeric value into a real utility with zero infinitesimal"""
        return Utility(value, 0.0)

    @staticmethod
    def from_name(name: str, real: bool) -> Utility:
        """convert a string into a utility, either `real` or infinitesimal"""
        variable = z3.Real(name)
        return Utility(variable, 0.0) if real else Utility(0.0, variable)

    def __repr__(self) -> str:
        return f"<{self.real}, {self.inf}>"

    def __neg__(self) -> Utility:
        return Utility(-self.real, -self.inf)

    def __add__(self, other: Union[int, float, Utility]) -> Utility:
        return self._binary_expression(other, add)

    def __radd__(self, other: Union[int, float, Utility]) -> Utility:
        """useful when parsing e.g. 2 + p"""
        return self._binary_expression(other, flip(add))

    def __sub__(self, other: Union[int, float, Utility]) -> Utility:
        return self._binary_expression(other, sub)

    def __rsub__(self, other: Union[int, float, Utility]) -> Utility:
        """useful when parsing e.g. 2 - p"""
        return self._binary_expression(other, flip(sub))

    def __mul__(self, other: Union[int, float, Utility]) -> Utility:
        """(x, a)*(y, b) = (xy, xa + yb + ab) ignores infinitesimals of order 2 """
      
        if isinstance(other, int) or isinstance(other, float):
            other = Utility.from_real(other)

        return   Utility(
            mul(self.real, other.real),
            add(mul(self.real, other.inf), mul(other.real,self.inf))
            )
        

    def __rmul__(self, other: Union[int, float, Utility]) -> Utility:
        """useful when parsing e.g. 2 * p"""

        if isinstance(other, int) or isinstance(other, float):
            other = Utility.from_real(other)

        return   Utility(
            mul(self.real, other.real),
            add(mul(self.real, other.inf), mul(other.real,self.inf))
            )

    def __truediv__(self, other: Union[int, float, Utility]) -> Utility:
        """(x, a)/(y, b) = (z,c), where (z,c)*(y,b)=(x,a) ignores infinitesimals of order 2"""
      
        if isinstance(other, int) or isinstance(other, float):
            other = Utility.from_real(other)

        return   Utility(
            div(self.real,other.real),
            div(sub(self.inf, mul(other.inf, div(self.real, other.real))), other.real)
            )

    def __rtruediv__(self, other: Union[int, float, Utility]) -> Utility: #ask michael
        """(x, a)/(y, b) = (z,c), where (z,c)*(y,b)=(x,a)"""
      
        if isinstance(other, int) or isinstance(other, float):
            other = Utility.from_real(other)

        return   Utility(
            div(other.real,self.real),
            div(sub(other.inf, mul(self.inf, div(other.real, self.real))), self.real)
            )
    

    def __pow__(self, other: Union[int, float]) -> Utility:
        """only real exponentiation, no utilities"""

        return Utility(
            pow(self.real, other),
            mul(mul(other, pow(self.real, other -1)), self.inf)
            )


    def __eq__(
            self,
            other: Union[int, float, Utility],
            label_fn: LabelFn = None
    ) -> z3.BoolRef:
        """
        generate a Z3 constraint `left == right`

        when `label_fn` is supplied, label generated comparisons for unsat cores
        """
        if isinstance(other, int) or isinstance(other, float):
            other = Utility.from_real(other)

        return conjunction(
            label(self.real, other.real, operator.eq, label_fn, True),
            label(self.inf, other.inf, operator.eq, label_fn, False)
        )

    def __ne__(
            self,
            other: Union[int, float, Utility],
            label_fn: LabelFn = None
    ) -> z3.BoolRef:
        """`z3.Not(left == right)`"""
        return negation(self.__eq__(other, label_fn))

    def __gt__(
            self,
            other: Union[int, float, Utility],
            label_fn: LabelFn = None
    ) -> z3.BoolRef:
        """
        generate a Z3 constraint `left > right`

        when `label_fn` is supplied, label generated comparisons for unsat cores
        """
        return self._binary_comparison(
            other, operator.gt, operator.gt, label_fn
        )

    def __ge__(
            self,
            other: Union[int, float, Utility],
            label_fn: LabelFn = None
    ) -> z3.BoolRef:
        """
        generate a Z3 constraint `left >= right`

        when `label_fn` is supplied, label generated comparisons for unsat cores
        """
        return self._binary_comparison(
            other, operator.gt, operator.ge, label_fn
        )

    def __lt__(
            self,
            other: Union[int, float, Utility],
            label_fn: LabelFn = None
    ) -> z3.BoolRef:
        """
        generate a Z3 constraint `left < right`

        when `label_fn` is supplied, label generated comparisons for unsat cores
        """
        return self._binary_comparison(
            other, operator.lt, operator.lt, label_fn
        )

    def __le__(
            self,
            other: Union[int, float, Utility],
            label_fn: LabelFn = None
    ) -> z3.BoolRef:
        """
        generate a Z3 constraint `left <= right`

        when `label_fn` is supplied, label generated comparisons for unsat cores
        """
        return self._binary_comparison(
            other, operator.lt, operator.le, label_fn
        )

    def _binary_expression(
            self,
            other: Union[int, float, Utility],
            op: Callable[[Real, Real], Real]
    ) -> Utility:
        """generate a Z3 expression `left op right`"""
        if isinstance(other, int) or isinstance(other, float):
            other = Utility.from_real(other)

        return Utility(
            op(self.real, other.real),
            op(self.inf, other.inf)
        )

    def _binary_comparison(
            self,
            other: Union[int, float, Utility],
            real_op: Callable[[Real, Real], Boolean],
            inf_op: Callable[[Real, Real], Boolean],
            label_fn: LabelFn = None
    ) -> z3.BoolRef:
        """
        generate a Z3 constraint `left op right` using `real_op` and `inf_op` parts

        when `label_fn` is supplied, label generated comparisons for unsat cores
        """
        if isinstance(other, int) or isinstance(other, float):
            other = Utility.from_real(other)

        return disjunction(
            label(self.real, other.real, real_op, label_fn, True),
            conjunction(
                label(self.real, other.real, operator.eq, label_fn, True),
                label(self.inf, other.inf, inf_op, label_fn, False)
            )
        )


ZERO = Utility.from_real(0.0)
"""the zero utility, <0.0, 0.0>"""

utility.py
sophierain/contract2game