From 08197d72a28f536aec03baa8231cc0dd9b549ec4 Mon Sep 17 00:00:00 2001
From: agatha <agatha@juggalol.com>
Date: Fri, 24 Nov 2023 13:40:03 -0500
Subject: [PATCH] Solve verilog challenge with Z3 theorem solver

---
 intro/skilift/README.md |  3 ++-
 intro/skilift/solver.py | 41 +++++++++++++++++++++++++++++++++++++++++
 2 files changed, 43 insertions(+), 1 deletion(-)
 create mode 100644 intro/skilift/solver.py

diff --git a/intro/skilift/README.md b/intro/skilift/README.md
index dba9606..54d73ea 100644
--- a/intro/skilift/README.md
+++ b/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
 ```
diff --git a/intro/skilift/solver.py b/intro/skilift/solver.py
new file mode 100644
index 0000000..fceb71d
--- /dev/null
+++ b/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.")
\ No newline at end of file