Solve verilog challenge with Z3 theorem solver

intro/skilift/README.md

@@ -1,4 +1,5 @@
-You arrive at the base station of a ski lift. Unfortunately for you, the lift is not in operation but you have to reach the next summit somehow. You enter the control room to find a control terminal with the words "Please input your key:"
+You arrive at the base station of a ski lift. Unfortunately for you, the lift is not in operation but you have to reach
+the next summit somehow. You enter the control room to find a control terminal with the words "Please input your key:"
 
 author: mole99
 ```

intro/skilift/solver.py

@@ -0,0 +1,41 @@
+from z3 import *
+
+# Create a Z3 BitVec variable for key
+key = BitVec('key', 64)
+
+# Create Z3 variables for tmp1, tmp2, tmp3, tmp4
+tmp1 = BitVec('tmp1', 64)
+tmp2 = BitVec('tmp2', 64)
+tmp3 = BitVec('tmp3', 64)
+tmp4 = BitVec('tmp4', 64)
+
+# Create a Z3 Solver instance
+solver = Solver()
+
+# Stage 1
+stage1_formula = tmp1 == (key & 0xF0F0F0F0F0F0F0F0)
+solver.add(stage1_formula)
+
+# Stage 2
+stage2_formula = tmp2 == ((tmp1 << 5) & 0xFFFFFFFFFFFFFFFF)
+solver.add(stage2_formula)
+
+# Stage 3
+stage3_formula = tmp3 == (tmp2 ^ 0x4841434B45525321)
+solver.add(stage3_formula)
+
+# Stage 4
+stage4_formula = tmp4 == (tmp3 - 12345678)
+solver.add(stage4_formula)
+
+# Final constraint
+final_constraint = tmp4 == 0x5443474D489DFDD3
+solver.add(final_constraint)
+
+# Check for a solution
+if solver.check() == sat:
+    model = solver.model()
+    key_value = model[key].as_long()
+    print(f"The correct value of key is: {hex(key_value)}")
+else:
+    print("No solution found.")