ianklatzco/ghidra-disassembly.c

## ghidra-disassembly.c

undefined8 check_secret_id(char *user_input)

{
  int iVar1;
  int iVar2;
  int user_input_(int);
  long lVar3;
  size_t sVar4;
  size_t sVar5;
  size_t sVar6;
  int bottom_four_numbers;
  int all_but_the_bottom_five_numbers;

  lVar3 = strtol(user_input,(char **)0x0,10);
  user_input_(int) = (int)lVar3;
  sVar4 = strlen(user_input);
  if ((SUB168((ZEXT816(0) << 0x40 | ZEXT816((ulong)(long)user_input_(int))) % ZEXT816(sVar4 + 2),0)
       == 0) && (user_input[4] == '1')) {
    all_but_the_bottom_five_numbers = user_input_(int) / 100000;
      // aka user_input[n]:user_input[5]
    bottom_four_numbers = user_input_(int) % 10000;
    if (((user_input[1] + user_input[3] * 10) - (( user_input[n:8] ) * 10 + user_input[5]) == 1 )
      // u[3] u[1] - 85 == 1
      // 12345678
      // 90618006
      //   69 68
      &&
      (((user_input[7])) * 10 + user_input[6] + (user_input[2] + (user_input[1] * 10) * -2 == 8))
      (
        76 +
        ( 2 + (1 * 10) * -2 == 8))
        // 7 + 8 == 8 // if == is higher prec, should return 8
                      // if == is lower prec, should return 0


              (((all_but_the_bottom_five_numbers / 100) % 10) * 10 +
              (all_but_the_bottom_five_numbers / 10) % 10 +
              ((bottom_four_numbers % 1000) / 100 + ((bottom_four_numbers % 100) / 10) * 10) * -2 ==
              8)

      // 76 - 12*2 == 8
      {
      iVar1 = (all_but_the_bottom_five_numbers % 10) * 10 + (all_but_the_bottom_five_numbers / 100) % 10;
      iVar2 = ((bottom_four_numbers / 100) % 10) * 10 + bottom_four_numbers % 10;
      if ((iVar1 / iVar2 == 3) && (iVar1 % iVar2 == 0)) {
        sVar4 = strlen(user_input);
        sVar5 = strlen(user_input);
        sVar6 = strlen(user_input);
        if ((long)(user_input_(int) % (all_but_the_bottom_five_numbers * bottom_four_numbers)) ==
            (sVar6 + 2) * (sVar4 + 2) * (sVar5 + 2) + 6) {
          return 1;
        }
      }
    }
  }
  return 0;
}


## iterate.c
#include <stdio.h>
#include <stdint.h>
#include <sys/mman.h>
#include <errno.h>
#include <sys/types.h>
#include <sys/stat.h>
#include <fcntl.h>
#include <string.h>
#include <stdlib.h>
#include <signal.h>

// This is a C harness that runs a patched ASM function that was taken from the
// binary, `silkroad.elf`.

// The patched function accepts a string of integers (max len 9) via rdi.
// It runs against a few constraints (roughly, each basic block in `bin`).
// If it fails any check, it returns back to the C handler.
// If it passes (reaches the call to puts), it exits, printing the correct
// number.
// I pulled it out of r2 using one of the pc?

// I have provided a statically compiled binary, `iterate`.

// This harness has an underlying challenge: every recompile, you'll need to
// update addresses to lib functions in the file `bin`.

// Specifically, the first 0x200 bytes have a few jmps to required lib functions.
// I wonder if I could've just inline asm'd the whole thing instead of mmap'ing
// a bin.... would've probably required a syntax transfer.


// Load some functions we'll want easy access to.
// I grabbed their addresses by disas'ing whatever in gdb, then using r2 to
// write the addresses to jmp to.
int whatever()
{
	char h[] = "hello\0";
	strtol((char *)-1, 0, 10);
	int c = strcmp(h,h);
	puts(h);
	return strlen(h) + c;
}


int main()
{
	signal(SIGFPE, SIG_IGN); // Attempt to suppress divide by 0 exceptions.
	// This worked for the first one, but I think ran into issues after there was
	// more than one.

	char arr[10] = {0};

	// File containing the "borrowed" function that we want to instrument.
	int f = open("bin", O_RDONLY);

	// mmap it into memory. It won't get loaded at 0x401000 (staticly compiled).
	void* new_region = mmap((int*)0x00401000, 1000, PROT_READ | PROT_WRITE |
		PROT_EXEC, MAP_PRIVATE, f, 0);
	if (new_region == (int*)-1)
	{
		printf("%d", errno);
		exit(69);
	}

	int ret;

	// Mark it as writeable/executable. Not necessary.
	ret = mprotect((int*)0x00400000, 0x1000, PROT_READ | PROT_WRITE | PROT_EXEC);
	if (ret == -1)
	{
		printf("mprotect 2 failed: errno %d", errno);
		exit(69);
	}

	// Iterate through possible values, including with variable amounts of
	// leading zeroes. Obtained by reversing the function w/ Ghidra.
	// Thanks, Kyle.

	// The most significant number is at the higher index of the string.
	// 0 1 2 3 4 5 6 7 8 9

	// totlen: [5,9]. Used to 0 pad the front of the string.
	for (int totlen=5; totlen <10; totlen++) {

		// Fill string w 0s.
		for (int j = 0; j < totlen; j++) {
			arr[j] = 0x30;
		}

		int ind_non_nine = -1;

		while (1) {

			// From the highest index to the lowest, find the first non-nine.
			ind_non_nine = -1;
			for (int i = totlen-1; i>=0; i--)
			{
				if (arr[i] != 0x39)
				{
					ind_non_nine = i;
					break;
				}
			}

			// If all nines, break to add a digit on the left.
			if (ind_non_nine == -1) {break;}

			// If you need to carry, carry.
			// 00009 -> 00000
			for (int i = totlen-1; i > ind_non_nine; i--) {
				arr[i] = 0x30;
			}

			arr[ind_non_nine]++;

			// At this point you have a new number.
			// Time to throw it into the instrumented code.

			// avoid div by 0 cases.
			if ( arr[totlen-3] == '0' && arr[totlen-1] == '0')
			{
				continue;
			}

			// nops to make it easier to find the address of this in gdb.
			asm("nop"); asm("nop"); asm("nop");

			// Transfer control flow to the ASM.

			  // RDI needs to contain the buffer
			  asm(
				"lea %0, %%rdi \n\t"
				"call %1"
					:"=m"(arr)  // hm, it's =m instead of =r.
					:"r"(new_region+0x40a)
				);
			asm("nop"); asm("nop"); asm("nop");

		}
	}
}


## my_angr.py
# first attempt at using z3 to just get to a partic address.
# result: angr says it can't find the thing.
# next: try expressing everything in z3's SMT language. basically what we did with python, but use a constraint solver instead of brute force.

import angr
import sys

def main(argv):
  # Create an Angr project.
  path_to_binary = 'silkroad.elf'  # :string
  project = angr.Project(path_to_binary, auto_load_libs=False)

  # Tell Angr where to start executing (should it start from the main()
  # function or somewhere else?) For now, use the entry_state function
  # to instruct Angr to start from the main() function.
  initial_state = project.factory.entry_state() # entry_state means main

  # Create a simulation manager initialized with the starting state. It provides
  # a number of useful tools to search and execute the binary.
  simulation = project.factory.simgr(initial_state)

  # addr of code that prints the thing we want
  print_good_address = 0x401aaf
  simulation.explore(find=print_good_address)
  # this will return a list of states that might be correct that get us to that eip

  # Check that we have found a solution. The simulation.explore() method will
  # set simulation.found to a list of the states that it could find that reach
  # the instruction we asked it to search for. Remember, in Python, if a list
  # is empty, it will be evaluated as false, otherwise true.
  if simulation.found:
    # The explore method stops after it finds a single state that arrives at the
    # target address.
    solution_state = simulation.found[0]

    # Print the string that Angr wrote to stdin to follow solution_state. This
    # is our solution.
    print solution_state.posix.dumps(sys.stdin.fileno())
  else:
    # If Angr could not find a path that reaches print_good_address, throw an
    # error. Perhaps you mistyped the print_good_address?
    raise Exception('Could not find the solution')

if __name__ == '__main__':
  main(sys.argv)

## solve.py
#!/usr/bin/python3
import random, sys, signal
import logging
from logging import *
import multiprocessing
basicConfig(level=DEBUG)

# I wrote this first, but got really confused with accessing various base10 digits of an int.
# So I wrote a C harness instead, iterate.c.

# this script doesn't test cases where there's leading 0s.
# as it turns out, that dousn't matter; tho i did find an interesting case that segfaults the binary.

# all of the checks that index, index from the rightmost side.
# eg: 790317143: check_2 asks for u[31].
# that is, ^ ^

# in:  [Int]
# out: Bool
def check_1( int_list = None, int_repr = None, strlen = None):
    a = int_repr % (strlen + 2)
    return a == 0

def check_2(int_repr=None, int_list=None, strlen = None, str_repr=None):
    # the fifth digit of the int from the right is '1'. (x0000)
    # u[4] == 1.
    # xxxx1xxxx
    return int_list[4] == 1

def check_3( int_list = None, int_repr = None, strlen = None, str_repr=None):
    # u[31] - u[85] == 1.
    l = int_list
    a = l[3]*10 + l[1] # 31
    b = l[8]*10 + l[5] # 85
    c = a-b # 31 - 85
    return c == 1

def check_4( int_list = None, int_repr = None, strlen = None ):
    # u[76] + u[12] * -2 == 8
    a = int_list[7] * 10 + int_list[6] # 76
    b = int_list[1] * 10 + int_list[2] # 12
    b = b * 2
    c = a - b
    return c == 8

def check_5( int_list = None, int_repr = None, strlen = None ):
    a = int_list[5] * 10 + int_list[7] # 57
    b = int_list[2] * 10 + int_list[0] # 20
    if b == 0: return False
    return (a / b == 3) and (a % b == 0)

def check_6( int_list = None, int_repr = None, strlen = None):
    top_numbers = int_repr // 100000 # // != / in py3. sigh. this caught me.
    bottom_nums = int_repr % 10000
    a = int_repr % (top_numbers * bottom_nums)
    b = strlen+2
    b = b*b*b +6
    return a == b

def worker(j):
    # 0,              1 000 000 000
    # 1 000 000 001,  2 000 000 000
    # 2 000 000 001,  3 000 000 000
    # 3 000 000 001,  4 000 000 000
    # 4 000 000 001,  4 294 967 295

    li = [0,0,0,0,0,0,0,0,0,0]

    # 9th position
    for i9 in range(0,5):
        for i7 in range(0,10):
            for i6 in range(0,10):
                for i3 in range(0,10):
                    for i2 in range(0,10):
                        for i1 in range(0,10):
                            for i0 in range(0,10):
                                if ( i3 == 0 and i1 == 0 ):
                                    # catch an edge case where u[31] < u[85] results in a div by 0
                                    continue
                                li[9] = i9
                                # i8
                                li[7] = i7
                                li[6] = i6
                                # i5
                                li[4] = 1  # check_2
                                li[3] = i3
                                li[2] = i2
                                li[1] = i1
                                li[0] = i0
                                # li = [0 1 2 3 x * 6 7 * 9] < MSD

                                # encode check_3 to get factor of ~100 speedup
                                # 31 - 1 = 85
                                eighty_five = (i3 * 10 + i1 - 1)
                                li[8] = eighty_five // 10
                                li[5] = eighty_five % 10

                                # li = li[::-1]
                                # 98765 4 3210 < c
                                # 01234 5 6789 < python
                                int_repr = li[9] * 1000000000 + \
                                    li[8] * 100000000 + \
                                    li[7] * 10000000 + \
                                    li[6] * 1000000 + \
                                    li[5] * 100000 + \
                                    li[4] * 10000 + \
                                    li[3] * 1000 + \
                                    li[2] * 100+ \
                                    li[1] * 10+ \
                                    li[0]

                                str_repr = str(int_repr)
                                strlen = len(str(int_repr))
                                int_list = [ x for x in map(int, str(int_repr).zfill(9)[::-1] ) ]

                                if ( \
                                        check_1(int_repr=int_repr, strlen = strlen, int_list=int_list) and\
                                        check_4(int_repr=int_repr, strlen = strlen, int_list=int_list) and \
                                        check_5(int_repr=int_repr, strlen = strlen, int_list=int_list) and \
                                        check_6(int_repr=int_repr, strlen = strlen, int_list=int_list) \
                                    ):
                                    # check_3(int_repr=int_repr, strlen = strlen, int_list=int_list) and \
                                    # check_2(int_repr=int_repr, strlen = strlen, int_list=int_list) and \
                                    # Can be totally omitted because of how we wrote our loop.
                                    print(li)
                                    print(int_repr)


if __name__ == '__main__':
    if (sys.version_info < (3,0)):
        print("wrong python version, use 3")
        sys.exit()
    # jobs = []
    # for x in range(0,4):
    #     print("Starting process " + str(x))
    #     p = multiprocessing.Process(target=worker, args=(x,))
    #     jobs.append(p)
    #     p.start()
    worker(0) # no need for multiprocess, optimized it well enough that it only takes a minute.

# 790317143
# also found this one that is NOT a right answer: 08901000 but will SIGFPE the binary
def check_answer(int_repr):
    str_repr = str(int_repr)
    strlen = len(str(int_repr))
    int_list = [ x for x in map(int, str(int_repr)[::-1] ) ]

    one = check_1(int_repr=int_repr, strlen = strlen, int_list=int_list)
    print("check 1: " + str(one))

    two = check_2(int_repr=int_repr, strlen = strlen, int_list=int_list, str_repr=str_repr)
    print("check 2: " + str(two))

    three = check_3(int_repr=int_repr, strlen = strlen, int_list=int_list, str_repr=str_repr)
    print("check 3: " + str(three))

    four = check_4(int_repr=int_repr, strlen = strlen, int_list=int_list)
    print("check 4: " + str(four))

    five = check_5(int_repr=int_repr, strlen = strlen, int_list=int_list)
    print("check 5: " + str(five))

    six = check_6(int_repr=int_repr, strlen = strlen, int_list=int_list)
    print("check 6: " + str(six))


## solve.z3
; first attempt at z3 to solve this problem.
; this script does not work.

(declare-const a String) ; "1234"
(declare-const b Int)    ; 1234 == 0x4d2

; b must be positive
(assert (>= b 0))

; b is int(a)
(assert (= (str.to.int a) b))

; a must be <=10
(assert (<= (str.len a) 10))

; len(a) + 2
(assert (= (+ (str.len a) 2) 12 ))

; a = i % (len(str(i)) + 2) # remainder
; return a == 0
(assert
  (= (mod b (+ (str.len a) 2)) 0)
)
; upon adding this check, z3 runs pretty much forever.

(check-sat)
(get-model)

	undefined8 check_secret_id(char *user_input)

	{
	int iVar1;
	int iVar2;
	int user_input_(int);
	long lVar3;
	size_t sVar4;
	size_t sVar5;
	size_t sVar6;
	int bottom_four_numbers;
	int all_but_the_bottom_five_numbers;

	lVar3 = strtol(user_input,(char **)0x0,10);
	user_input_(int) = (int)lVar3;
	sVar4 = strlen(user_input);
	if ((SUB168((ZEXT816(0) << 0x40 \| ZEXT816((ulong)(long)user_input_(int))) % ZEXT816(sVar4 + 2),0)
	== 0) && (user_input[4] == '1')) {
	all_but_the_bottom_five_numbers = user_input_(int) / 100000;
	// aka user_input[n]:user_input[5]
	bottom_four_numbers = user_input_(int) % 10000;
	if (((user_input[1] + user_input[3] * 10) - (( user_input[n:8] ) * 10 + user_input[5]) == 1 )
	// u[3] u[1] - 85 == 1
	// 12345678
	// 90618006
	// 69 68
	&&
	(((user_input[7])) * 10 + user_input[6] + (user_input[2] + (user_input[1] * 10) * -2 == 8))
	(
	76 +
	( 2 + (1 * 10) * -2 == 8))
	// 7 + 8 == 8 // if == is higher prec, should return 8
	// if == is lower prec, should return 0


	(((all_but_the_bottom_five_numbers / 100) % 10) * 10 +
	(all_but_the_bottom_five_numbers / 10) % 10 +
	((bottom_four_numbers % 1000) / 100 + ((bottom_four_numbers % 100) / 10) * 10) * -2 ==
	8)

	// 76 - 12*2 == 8
	{
	iVar1 = (all_but_the_bottom_five_numbers % 10) * 10 + (all_but_the_bottom_five_numbers / 100) % 10;
	iVar2 = ((bottom_four_numbers / 100) % 10) * 10 + bottom_four_numbers % 10;
	if ((iVar1 / iVar2 == 3) && (iVar1 % iVar2 == 0)) {
	sVar4 = strlen(user_input);
	sVar5 = strlen(user_input);
	sVar6 = strlen(user_input);
	if ((long)(user_input_(int) % (all_but_the_bottom_five_numbers * bottom_four_numbers)) ==
	(sVar6 + 2) * (sVar4 + 2) * (sVar5 + 2) + 6) {
	return 1;
	}
	}
	}
	}
	return 0;
	}
	#include <stdio.h>
	#include <stdint.h>
	#include <sys/mman.h>
	#include <errno.h>
	#include <sys/types.h>
	#include <sys/stat.h>
	#include <fcntl.h>
	#include <string.h>
	#include <stdlib.h>
	#include <signal.h>

	// This is a C harness that runs a patched ASM function that was taken from the
	// binary, `silkroad.elf`.

	// The patched function accepts a string of integers (max len 9) via rdi.
	// It runs against a few constraints (roughly, each basic block in `bin`).
	// If it fails any check, it returns back to the C handler.
	// If it passes (reaches the call to puts), it exits, printing the correct
	// number.
	// I pulled it out of r2 using one of the pc?

	// I have provided a statically compiled binary, `iterate`.

	// This harness has an underlying challenge: every recompile, you'll need to
	// update addresses to lib functions in the file `bin`.

	// Specifically, the first 0x200 bytes have a few jmps to required lib functions.
	// I wonder if I could've just inline asm'd the whole thing instead of mmap'ing
	// a bin.... would've probably required a syntax transfer.



	// Load some functions we'll want easy access to.
	// I grabbed their addresses by disas'ing whatever in gdb, then using r2 to
	// write the addresses to jmp to.
	int whatever()
	{
	char h[] = "hello\0";
	strtol((char *)-1, 0, 10);
	int c = strcmp(h,h);
	puts(h);
	return strlen(h) + c;
	}


	int main()
	{
	signal(SIGFPE, SIG_IGN); // Attempt to suppress divide by 0 exceptions.
	// This worked for the first one, but I think ran into issues after there was
	// more than one.

	char arr[10] = {0};

	// File containing the "borrowed" function that we want to instrument.
	int f = open("bin", O_RDONLY);

	// mmap it into memory. It won't get loaded at 0x401000 (staticly compiled).
	void* new_region = mmap((int*)0x00401000, 1000, PROT_READ \| PROT_WRITE \|
	PROT_EXEC, MAP_PRIVATE, f, 0);
	if (new_region == (int*)-1)
	{
	printf("%d", errno);
	exit(69);
	}

	int ret;

	// Mark it as writeable/executable. Not necessary.
	ret = mprotect((int*)0x00400000, 0x1000, PROT_READ \| PROT_WRITE \| PROT_EXEC);
	if (ret == -1)
	{
	printf("mprotect 2 failed: errno %d", errno);
	exit(69);
	}

	// Iterate through possible values, including with variable amounts of
	// leading zeroes. Obtained by reversing the function w/ Ghidra.
	// Thanks, Kyle.

	// The most significant number is at the higher index of the string.
	// 0 1 2 3 4 5 6 7 8 9

	// totlen: [5,9]. Used to 0 pad the front of the string.
	for (int totlen=5; totlen <10; totlen++) {

	// Fill string w 0s.
	for (int j = 0; j < totlen; j++) {
	arr[j] = 0x30;
	}

	int ind_non_nine = -1;

	while (1) {

	// From the highest index to the lowest, find the first non-nine.
	ind_non_nine = -1;
	for (int i = totlen-1; i>=0; i--)
	{
	if (arr[i] != 0x39)
	{
	ind_non_nine = i;
	break;
	}
	}

	// If all nines, break to add a digit on the left.
	if (ind_non_nine == -1) {break;}

	// If you need to carry, carry.
	// 00009 -> 00000
	for (int i = totlen-1; i > ind_non_nine; i--) {
	arr[i] = 0x30;
	}

	arr[ind_non_nine]++;

	// At this point you have a new number.
	// Time to throw it into the instrumented code.

	// avoid div by 0 cases.
	if ( arr[totlen-3] == '0' && arr[totlen-1] == '0')
	{
	continue;
	}

	// nops to make it easier to find the address of this in gdb.
	asm("nop"); asm("nop"); asm("nop");

	// Transfer control flow to the ASM.

	// RDI needs to contain the buffer
	asm(
	"lea %0, %%rdi \n\t"
	"call %1"
	:"=m"(arr) // hm, it's =m instead of =r.
	:"r"(new_region+0x40a)
	);
	asm("nop"); asm("nop"); asm("nop");

	}
	}
	}
	# first attempt at using z3 to just get to a partic address.
	# result: angr says it can't find the thing.
	# next: try expressing everything in z3's SMT language. basically what we did with python, but use a constraint solver instead of brute force.

	import angr
	import sys

	def main(argv):
	# Create an Angr project.
	path_to_binary = 'silkroad.elf' # :string
	project = angr.Project(path_to_binary, auto_load_libs=False)

	# Tell Angr where to start executing (should it start from the main()
	# function or somewhere else?) For now, use the entry_state function
	# to instruct Angr to start from the main() function.
	initial_state = project.factory.entry_state() # entry_state means main

	# Create a simulation manager initialized with the starting state. It provides
	# a number of useful tools to search and execute the binary.
	simulation = project.factory.simgr(initial_state)

	# addr of code that prints the thing we want
	print_good_address = 0x401aaf
	simulation.explore(find=print_good_address)
	# this will return a list of states that might be correct that get us to that eip

	# Check that we have found a solution. The simulation.explore() method will
	# set simulation.found to a list of the states that it could find that reach
	# the instruction we asked it to search for. Remember, in Python, if a list
	# is empty, it will be evaluated as false, otherwise true.
	if simulation.found:
	# The explore method stops after it finds a single state that arrives at the
	# target address.
	solution_state = simulation.found[0]

	# Print the string that Angr wrote to stdin to follow solution_state. This
	# is our solution.
	print solution_state.posix.dumps(sys.stdin.fileno())
	else:
	# If Angr could not find a path that reaches print_good_address, throw an
	# error. Perhaps you mistyped the print_good_address?
	raise Exception('Could not find the solution')

	if __name__ == '__main__':
	main(sys.argv)
	#!/usr/bin/python3
	import random, sys, signal
	import logging
	from logging import *
	import multiprocessing
	basicConfig(level=DEBUG)

	# I wrote this first, but got really confused with accessing various base10 digits of an int.
	# So I wrote a C harness instead, iterate.c.

	# this script doesn't test cases where there's leading 0s.
	# as it turns out, that dousn't matter; tho i did find an interesting case that segfaults the binary.

	# all of the checks that index, index from the rightmost side.
	# eg: 790317143: check_2 asks for u[31].
	# that is, ^ ^

	# in: [Int]
	# out: Bool
	def check_1( int_list = None, int_repr = None, strlen = None):
	a = int_repr % (strlen + 2)
	return a == 0

	def check_2(int_repr=None, int_list=None, strlen = None, str_repr=None):
	# the fifth digit of the int from the right is '1'. (x0000)
	# u[4] == 1.
	# xxxx1xxxx
	return int_list[4] == 1

	def check_3( int_list = None, int_repr = None, strlen = None, str_repr=None):
	# u[31] - u[85] == 1.
	l = int_list
	a = l[3]*10 + l[1] # 31
	b = l[8]*10 + l[5] # 85
	c = a-b # 31 - 85
	return c == 1

	def check_4( int_list = None, int_repr = None, strlen = None ):
	# u[76] + u[12] * -2 == 8
	a = int_list[7] * 10 + int_list[6] # 76
	b = int_list[1] * 10 + int_list[2] # 12
	b = b * 2
	c = a - b
	return c == 8

	def check_5( int_list = None, int_repr = None, strlen = None ):
	a = int_list[5] * 10 + int_list[7] # 57
	b = int_list[2] * 10 + int_list[0] # 20
	if b == 0: return False
	return (a / b == 3) and (a % b == 0)

	def check_6( int_list = None, int_repr = None, strlen = None):
	top_numbers = int_repr // 100000 # // != / in py3. sigh. this caught me.
	bottom_nums = int_repr % 10000
	a = int_repr % (top_numbers * bottom_nums)
	b = strlen+2
	b = bbb +6
	return a == b

	def worker(j):
	# 0, 1 000 000 000
	# 1 000 000 001, 2 000 000 000
	# 2 000 000 001, 3 000 000 000
	# 3 000 000 001, 4 000 000 000
	# 4 000 000 001, 4 294 967 295

	li = [0,0,0,0,0,0,0,0,0,0]

	# 9th position
	for i9 in range(0,5):
	for i7 in range(0,10):
	for i6 in range(0,10):
	for i3 in range(0,10):
	for i2 in range(0,10):
	for i1 in range(0,10):
	for i0 in range(0,10):
	if ( i3 == 0 and i1 == 0 ):
	# catch an edge case where u[31] < u[85] results in a div by 0
	continue
	li[9] = i9
	# i8
	li[7] = i7
	li[6] = i6
	# i5
	li[4] = 1 # check_2
	li[3] = i3
	li[2] = i2
	li[1] = i1
	li[0] = i0
	# li = [0 1 2 3 x * 6 7 * 9] < MSD

	# encode check_3 to get factor of ~100 speedup
	# 31 - 1 = 85
	eighty_five = (i3 * 10 + i1 - 1)
	li[8] = eighty_five // 10
	li[5] = eighty_five % 10

	# li = li[::-1]
	# 98765 4 3210 < c
	# 01234 5 6789 < python
	int_repr = li[9] * 1000000000 + \
	li[8] * 100000000 + \
	li[7] * 10000000 + \
	li[6] * 1000000 + \
	li[5] * 100000 + \
	li[4] * 10000 + \
	li[3] * 1000 + \
	li[2] * 100+ \
	li[1] * 10+ \
	li[0]

	str_repr = str(int_repr)
	strlen = len(str(int_repr))
	int_list = [ x for x in map(int, str(int_repr).zfill(9)[::-1] ) ]

	if ( \
	check_1(int_repr=int_repr, strlen = strlen, int_list=int_list) and\
	check_4(int_repr=int_repr, strlen = strlen, int_list=int_list) and \
	check_5(int_repr=int_repr, strlen = strlen, int_list=int_list) and \
	check_6(int_repr=int_repr, strlen = strlen, int_list=int_list) \
	):
	# check_3(int_repr=int_repr, strlen = strlen, int_list=int_list) and \
	# check_2(int_repr=int_repr, strlen = strlen, int_list=int_list) and \
	# Can be totally omitted because of how we wrote our loop.
	print(li)
	print(int_repr)



	if __name__ == '__main__':
	if (sys.version_info < (3,0)):
	print("wrong python version, use 3")
	sys.exit()
	# jobs = []
	# for x in range(0,4):
	# print("Starting process " + str(x))
	# p = multiprocessing.Process(target=worker, args=(x,))
	# jobs.append(p)
	# p.start()
	worker(0) # no need for multiprocess, optimized it well enough that it only takes a minute.

	# 790317143
	# also found this one that is NOT a right answer: 08901000 but will SIGFPE the binary
	def check_answer(int_repr):
	str_repr = str(int_repr)
	strlen = len(str(int_repr))
	int_list = [ x for x in map(int, str(int_repr)[::-1] ) ]

	one = check_1(int_repr=int_repr, strlen = strlen, int_list=int_list)
	print("check 1: " + str(one))

	two = check_2(int_repr=int_repr, strlen = strlen, int_list=int_list, str_repr=str_repr)
	print("check 2: " + str(two))

	three = check_3(int_repr=int_repr, strlen = strlen, int_list=int_list, str_repr=str_repr)
	print("check 3: " + str(three))

	four = check_4(int_repr=int_repr, strlen = strlen, int_list=int_list)
	print("check 4: " + str(four))

	five = check_5(int_repr=int_repr, strlen = strlen, int_list=int_list)
	print("check 5: " + str(five))

	six = check_6(int_repr=int_repr, strlen = strlen, int_list=int_list)
	print("check 6: " + str(six))
	; first attempt at z3 to solve this problem.
	; this script does not work.

	(declare-const a String) ; "1234"
	(declare-const b Int) ; 1234 == 0x4d2

	; b must be positive
	(assert (>= b 0))

	; b is int(a)
	(assert (= (str.to.int a) b))

	; a must be <=10
	(assert (<= (str.len a) 10))

	; len(a) + 2
	(assert (= (+ (str.len a) 2) 12 ))

	; a = i % (len(str(i)) + 2) # remainder
	; return a == 0
	(assert
	(= (mod b (+ (str.len a) 2)) 0)
	)
	; upon adding this check, z3 runs pretty much forever.

	(check-sat)
	(get-model)