# Path: parser/stpcommands.py
# def blockCharacteristic(stpfile, characteristic, wordsize):
# def setupQuery(stpfile):
# def setupVariables(stpfile, variables, wordsize):
# def assertVariableValue(stpfile, a, b):
# def getStringForVariables(variables, wordsize):
# def assertNonZero(stpfile, variables, wordsize):
# def getStringForNonZero(variables, wordsize):
# def limitWeight(stpfile, weight, p, wordsize, ignoreMSBs=0):
# def setupWeightComputationSum(stpfile, weight, p, wordsize, ignoreMSBs=0):
# def setupWeightComputation(stpfile, weight, p, wordsize, ignoreMSBs=0):
# def getWeightString(variables, wordsize, ignoreMSBs=0, weightVariable="weight"):
# def getStringEq(a, b, c):
# def getStringAdd(a, b, c, wordsize):
# def getStringForAndDifferential(a, b, c):
# def getStringLeftRotate(value, rotation, wordsize):
# def getStringRightRotate(value, rotation, wordsize):
# def add4bitSbox(sbox, variables):
#     DDT = [[0]*16 for i in range(16)]
# 
# Path: ciphers/cipher.py
# class AbstractCipher(object, metaclass=ABCMeta):
#     """
#     Abstract Class for Ciphers
#     """
# 
#     @abstractmethod
#     def createSTP(self, filename, cipherParameters):
#         """
#         Each cipher need to define how it creates an instance for the
#         SMT solver.
#         """
#         pass
# 
#     @abstractmethod
#     def getFormatString(self):
#         """
#         Each cipher needs to specify the format it should be printed.
#         """
#         pass
# 
# Path: parser/stpcommands.py
# def getStringLeftRotate(value, rotation, wordsize):
#     if rotation % wordsize == 0:
#         return "{0}".format(value)
#     command = "((({0} << {1})[{2}:0]) | (({0} >> {3})[{2}:0]))".format(
#         value, (rotation % wordsize), wordsize - 1, (wordsize - rotation) % wordsize)
# 
#     return command
# 
# Path: parser/stpcommands.py
# def getStringRightRotate(value, rotation, wordsize):
#     if rotation % wordsize == 0:
#         return "{0}".format(value)
#     command = "((({0} >> {1})[{2}:0]) | (({0} << {3})[{2}:0]))".format(
#         value, (rotation % wordsize), wordsize - 1, (wordsize - rotation) % wordsize)
#     return command


from parser import stpcommands
from ciphers.cipher import AbstractCipher
from parser.stpcommands import getStringLeftRotate as rotl
from parser.stpcommands import getStringRightRotate as rotr
    def setupKeySchedule(self, stp_file, key, tmp_key, rounds, wordsize):
        command = ""
        const3 = "0x{}3".format("0"*(wordsize // 4 - 1))
        if rounds > 4:
            for i in range(4, rounds):
                constz = "0x{}{}".format("0"*(wordsize // 4 - 1),
                                         self.CONST_Z[(i - 4) % 62])
                tmp = "BVXOR({}, {})".format(rotr(key[i-1], 3, wordsize), key[i-3])
                command += "ASSERT({} = BVXOR({}, {}));\n".format(
                    tmp_key[i], tmp, rotr(tmp, 1, wordsize))
                command += "ASSERT({} = BVXOR({}, BVXOR({}, BVXOR(~{}, {}))));\n".format(
                    key[i], constz, const3, key[i-4], tmp_key[i])
        stp_file.write(command)
        return

    def setupSimonRound(self, stp_file, x0_in, y0_in,  x0_out, y0_out,
                        and_out0, key, wordsize):
        """
        Returns a string representing one round of Simon in STP.
        y[i+1] = x[i]
        x[i+1] = (x[i] <<< 1) & (x[i] <<< 8) ^ y[i] ^ (x[i] << 2) ^ key
        """
        command = ""

        #Assert(y_out = x_in)
        command += "ASSERT({} = {});\n".format(y0_out, x0_in)

        #Assert AND Output
        command += "ASSERT({} = {} & {});\n".format(and_out0, 
            rotl(x0_in, self.rot_beta, wordsize), 

# Path: parser/stpcommands.py
# def blockCharacteristic(stpfile, characteristic, wordsize):
# def setupQuery(stpfile):
# def setupVariables(stpfile, variables, wordsize):
# def assertVariableValue(stpfile, a, b):
# def getStringForVariables(variables, wordsize):
# def assertNonZero(stpfile, variables, wordsize):
# def getStringForNonZero(variables, wordsize):
# def limitWeight(stpfile, weight, p, wordsize, ignoreMSBs=0):
# def setupWeightComputationSum(stpfile, weight, p, wordsize, ignoreMSBs=0):
# def setupWeightComputation(stpfile, weight, p, wordsize, ignoreMSBs=0):
# def getWeightString(variables, wordsize, ignoreMSBs=0, weightVariable="weight"):
# def getStringEq(a, b, c):
# def getStringAdd(a, b, c, wordsize):
# def getStringForAndDifferential(a, b, c):
# def getStringLeftRotate(value, rotation, wordsize):
# def getStringRightRotate(value, rotation, wordsize):
# def add4bitSbox(sbox, variables):
#     DDT = [[0]*16 for i in range(16)]
# 
# Path: ciphers/cipher.py
# class AbstractCipher(object, metaclass=ABCMeta):
#     """
#     Abstract Class for Ciphers
#     """
# 
#     @abstractmethod
#     def createSTP(self, filename, cipherParameters):
#         """
#         Each cipher need to define how it creates an instance for the
#         SMT solver.
#         """
#         pass
# 
#     @abstractmethod
#     def getFormatString(self):
#         """
#         Each cipher needs to specify the format it should be printed.
#         """
#         pass
# 
# Path: parser/stpcommands.py
# def getStringLeftRotate(value, rotation, wordsize):
#     if rotation % wordsize == 0:
#         return "{0}".format(value)
#     command = "((({0} << {1})[{2}:0]) | (({0} >> {3})[{2}:0]))".format(
#         value, (rotation % wordsize), wordsize - 1, (wordsize - rotation) % wordsize)
# 
#     return command
# 
# Path: parser/stpcommands.py
# def getStringRightRotate(value, rotation, wordsize):
#     if rotation % wordsize == 0:
#         return "{0}".format(value)
#     command = "((({0} >> {1})[{2}:0]) | (({0} << {3})[{2}:0]))".format(
#         value, (rotation % wordsize), wordsize - 1, (wordsize - rotation) % wordsize)
#     return command


# Path: ciphers/simonkeyrc.py
from parser import stpcommands
from ciphers.cipher import AbstractCipher
from parser.stpcommands import getStringLeftRotate as rotl
from parser.stpcommands import getStringRightRotate as rotr

    def setupKeySchedule(self, stp_file, key, tmp_key, rounds, wordsize):
        command = ""
        const3 = "0x{}3".format("0"*(wordsize // 4 - 1))
        if rounds > 4:
            for i in range(4, rounds):
                constz = "0x{}{}".format("0"*(wordsize // 4 - 1),
                                         self.CONST_Z[(i - 4) % 62])
                tmp = "BVXOR({}, {})".format(rotr(key[i-1], 3, wordsize), key[i-3])
                command += "ASSERT({} = BVXOR({}, {}));\n".format(
                    tmp_key[i], tmp, rotr(tmp, 1, wordsize))
                command += "ASSERT({} = BVXOR({}, BVXOR({}, BVXOR(~{}, {}))));\n".format(
                    key[i], constz, const3, key[i-4], tmp_key[i])
        stp_file.write(command)
        return

    def setupSimonRound(self, stp_file, x0_in, y0_in,  x0_out, y0_out,
                        and_out0, key, wordsize):
        """
        Returns a string representing one round of Simon in STP.
        y[i+1] = x[i]
        x[i+1] = (x[i] <<< 1) & (x[i] <<< 8) ^ y[i] ^ (x[i] << 2) ^ key
        """
        command = ""

        #Assert(y_out = x_in)
        command += "ASSERT({} = {});\n".format(y0_out, x0_in)

        #Assert AND Output
        command += "ASSERT({} = {} & {});\n".format(and_out0, 
            rotl(x0_in, self.rot_beta, wordsize), 

            rotl(x0_in, self.rot_alpha, wordsize))