How to solve this with z3?

Question

I just started writing scripts using z3 , only for CTF tasks.

for ( i = 0; i <= 7; ++i )
{
   s2[i] += s2[i] % 10;
   if ( s2[i] > 123 )
     s2[i] = -100 - s2[i];
}
strcmp("H0Tf00D:<", s2)

This is a fairly simple logic that can even be done manually. But since I am studying z3 , so I was wondering if this could be done or not using z3.

I did some of my homework in , if conditions using z3 , and not so much I found.

Here are some of the things I learned:

• Z3 Prover Github
• height4fun - manual
• z3-how-to-encode-if-the-else-in-z3-python
• z3py-tutorial - ericpony github

PS I don’t want a solution, I just want to know if it can be done with z3 or not, and if so, then point me in the right direction.

Update1

I have made a lot of progress (although this does nothing):

from z3 import *

s1 = Int('s[1]')
s2 = Int('s[2]')
s3 = Int('s[3]')
s4 = Int('s[4]')
s5 = Int('s[5]')
s6 = Int('s[6]')
s7 = Int('s[7]')

s = Solver()

a = "H0Tf00D:<"

Answer 1

, , ( ) , :

from z3 import *

def get_decoded(target):
    """
    Helper function to "decode" a target string using Z3
    """

    #
    # We create a Z3 array for the contents of the string (this saves
    # needing have multiple copies of the "s[i]" variables.
    #
    # However, this could be less efficient, but this isn't a concern for this
    # puzzle
    #
    string = Array("string", BitVecSort(32), BitVecSort(32))

    #
    # We save a copy of the string as the "initial" string, as we need to
    # interrogate the string _before_ the updates are made
    #    
    initial_string = string

    #
    # Create a Z3 solver
    #
    s = Solver()

    #
    # We now iterate over the length of the "target" string, and construct the
    # encoding as per the CTF instance
    #
    for idx in range(len(target)):
        #
        # Extract the single character at "idx" from the target string
        #
        single_c = target[idx]

        #
        # Find its ASCII value
        #
        ord_val = ord(single_c)

        #
        # Generate the corresponding Z3 constant
        #
        ord_const = BitVecVal(ord_val, 32)

        #
        # Generate the cell position as a Z3 constant
        #
        cell_pos = BitVecVal(idx, 32)

        #
        # Calculate the non-conditional part of the update
        #
        add_rem = string[cell_pos] + SRem(string[cell_pos], 10)

        #
        # Calculate the conditional part of the update using a Z3 If
        #
        to_store = If(add_rem > 123, -100 - add_rem, add_rem)

        #
        # Update the string with our calculated value
        #
        string = Store(string, idx, to_store)

        #
        # Assert that our calculated position is equal to the input value
        #
        s.add(string[cell_pos] == BitVecVal(ord_val, 32))

    #
    # Check the SMT instance and obtain the model
    #
    assert s.check() == sat
    model = s.model()

    #
    # We now interrogate the model to find out what the "original" string was
    #
    output = []

    #
    # Output string is the same length as the input string
    #
    for idx in range(len(target)):
        #
        # As before, calculate the cell position
        #
        cell_pos = BitVecVal(idx, 32)

        #
        # Extract the value for the index in the string
        #
        model_val = model.eval(initial_string[cell_pos]).as_signed_long()

        #
        # Get the ASCII value (we've stored the ASCII integer value, not the
        # char!)
        #
        model_char = chr(model_val)

        #
        # Append it to our output string
        #
        output.append(model_char)

    #
    # Return the joined string
    #
    return "".join(output)


def get_encoded(value):
    """
    Helper function to "encode" a string using Python
    """

    output = []

    #
    # Iterate over the input string
    #
    for idx in range(len(value)):
        #
        # Value at position (as ASCII int)
        #
        ord_val = ord(value[idx])

        #
        # Value we're going to store
        #  
        to_store = ord_val + ord_val % 10

        #
        # Conditional check
        #
        if to_store > 123:

            #
            # As per the CTF
            #
            to_store = -100 - to_store

        #
        # Add it to the output string
        #
        output.append(chr(to_store))

    #
    # Return it
    #
    return "".join(output)


if __name__ == "__main__":
    """
    Entry point
    """

    #
    # String we're aiming for
    #
    target = "H0Tf00D:<"
    print "Target:                   \"{:s}\"".format(target)

    #
    # Calculate the "reverse" using Z3
    #
    decoded = get_decoded(target)
    print "Decoded (via z3):         \"{:s}\"".format(decoded)

    #
    # We now re-encode
    #
    encoded = get_encoded(decoded)
    print "Encoded (via Python):     \"{:s}\"".format(encoded)

    #
    # Both strings should be equal
    #
    assert encoded == target

# EOF