# 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 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: 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


from parser import stpcommands
from ciphers.cipher import AbstractCipher
from parser.stpcommands import getStringRightRotate as rotr
from parser.stpcommands import getStringLeftRotate as rotl
        in0xorin2rr = rotr(in0xorin2, 8, wordsize)
        r = "BVXOR({0}, BVXOR({1}, {2}))".format(in0xorin2lr, in0xorin2, in0xorin2rr)

        command += "ASSERT({0}[31:0] = BVXOR({1}[31:0], {2}[31:0]));\n".format(out0, in0, l)
        command += "ASSERT({0}[31:0] = BVXOR({1}[31:0], {2}[31:0]));\n".format(out1, in1, r)
        command += "ASSERT({0}[31:0] = BVXOR({1}[31:0], {2}[31:0]));\n".format(out2, in2, l)
        command += "ASSERT({0}[31:0] = BVXOR({1}[31:0], {2}[31:0]));\n".format(out3, in3, r)

        return command

    def gamma(self, in0, in1, in2, in3, out0, out1, out2, out3, w):
        """
        Model for the Gamma function in NOEKEON - represents the Sbox layer
        """
        command = ""

        noekeon_sbox = [7, 0xA, 2, 0xC, 4, 8, 0xF, 0, 5, 9, 1, 0xE, 3, 0xD, 0xB, 6]
        for i in range(32):
            variables = ["{0}[{1}:{1}]".format(in3, i),
                         "{0}[{1}:{1}]".format(in2, i),
                         "{0}[{1}:{1}]".format(in1, i),
                         "{0}[{1}:{1}]".format(in0, i),
                         "{0}[{1}:{1}]".format(out3, i),
                         "{0}[{1}:{1}]".format(out2, i),
                         "{0}[{1}:{1}]".format(out1, i),
                         "{0}[{1}:{1}]".format(out0, i),
                         "{0}[{1}:{1}]".format(w, 4*i + 3),
                         "{0}[{1}:{1}]".format(w, 4*i + 2),
                         "{0}[{1}:{1}]".format(w, 4*i + 1),
                         "{0}[{1}:{1}]".format(w, 4*i + 0)]

# 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 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: 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: ciphers/noekeon.py
from parser import stpcommands
from ciphers.cipher import AbstractCipher
from parser.stpcommands import getStringRightRotate as rotr
from parser.stpcommands import getStringLeftRotate as rotl

        in0xorin2rr = rotr(in0xorin2, 8, wordsize)
        r = "BVXOR({0}, BVXOR({1}, {2}))".format(in0xorin2lr, in0xorin2, in0xorin2rr)

        command += "ASSERT({0}[31:0] = BVXOR({1}[31:0], {2}[31:0]));\n".format(out0, in0, l)
        command += "ASSERT({0}[31:0] = BVXOR({1}[31:0], {2}[31:0]));\n".format(out1, in1, r)
        command += "ASSERT({0}[31:0] = BVXOR({1}[31:0], {2}[31:0]));\n".format(out2, in2, l)
        command += "ASSERT({0}[31:0] = BVXOR({1}[31:0], {2}[31:0]));\n".format(out3, in3, r)

        return command

    def gamma(self, in0, in1, in2, in3, out0, out1, out2, out3, w):
        """
        Model for the Gamma function in NOEKEON - represents the Sbox layer
        """
        command = ""

        noekeon_sbox = [7, 0xA, 2, 0xC, 4, 8, 0xF, 0, 5, 9, 1, 0xE, 3, 0xD, 0xB, 6]
        for i in range(32):
            variables = ["{0}[{1}:{1}]".format(in3, i),
                         "{0}[{1}:{1}]".format(in2, i),
                         "{0}[{1}:{1}]".format(in1, i),
                         "{0}[{1}:{1}]".format(in0, i),
                         "{0}[{1}:{1}]".format(out3, i),
                         "{0}[{1}:{1}]".format(out2, i),
                         "{0}[{1}:{1}]".format(out1, i),
                         "{0}[{1}:{1}]".format(out0, i),
                         "{0}[{1}:{1}]".format(w, 4*i + 3),
                         "{0}[{1}:{1}]".format(w, 4*i + 2),
                         "{0}[{1}:{1}]".format(w, 4*i + 1),
                         "{0}[{1}:{1}]".format(w, 4*i + 0)]

            command += stpcommands.add4bitSbox(noekeon_sbox, variables)