def setupChasKeyRound(self, stp_file, rnd, v0_in, v1_in, v2_in, v3_in, v0_out,
                          v1_out, v2_out, v3_out, w0, w1, wordsize):

        """
        Half a round of ChasKey

        a0 = (v1 + v0) <<< 32
        a1 = (v1 + v0) ^ (v1 <<< 13)
        a2 = (v2 + v3)
        a3 = (v2 + v3) ^ (v3 <<< 16)
        """
        command = ""

        if (rnd % 2) == 0:
            rot_one = 5
            rot_two = 8
        else:
            rot_one = 7
            rot_two = 13

        #Assert intermediate values
        #Rotate right to get correct output value

        #v0_out
        command += "ASSERT("
        command += stpcommands.getStringAdd(v2_in, v3_in, v0_out, wordsize)
        command += ");\n"

        #v1_out
        command += "ASSERT({} = BVXOR({}, {}));\n".format(
            v1_out, rotl(v1_in, rot_one, wordsize), rotr(v2_out, 16, wordsize))

        #v2_out
        command += "ASSERT("
        command += stpcommands.getStringAdd(
            v1_in, v0_in, rotr(v2_out, 16, wordsize), wordsize)
        command += ");\n"

        #v3_out
        command += "ASSERT({} = BVXOR({}, {}));\n".format(
            v3_out, rotl(v3_in, rot_two, wordsize), v0_out)

        # Compute Weights for modular addition
        # Lipmaa and Moriai

        command += "ASSERT({0} = ~".format(w0)
        command += stpcommands.getStringEq(
            v1_in, v0_in, rotr(v2_out, 16, wordsize))
        command += ");\n"

        command += "ASSERT({0} = ~".format(w1)
        command += stpcommands.getStringEq(v2_in, v3_in, v0_out)
        command += ");\n"

        stp_file.write(command)
        return
dataset/ETHPy150Open kste/cryptosmt/ciphers/chaskeymachalf.py/ChasKeyMacHalf.setupChasKeyRound/original