diff --git a/.github/workflows/cbmc.yml b/.github/workflows/cbmc.yml
index cc2ed49..2246cdc 100644
--- a/.github/workflows/cbmc.yml
+++ b/.github/workflows/cbmc.yml
@@ -44,7 +44,7 @@ jobs:
           cd cbmc-src
           STRATA="$GITHUB_WORKSPACE/.lake/packages/Strata"
           git apply "$GITHUB_WORKSPACE/StrataPythonTest/cbmc-string-support.patch"
-          git apply "$STRATA/StrataTest/Languages/Laurel/cbmc-bounds-check.patch"
+          git apply "$STRATA/StrataTest/Languages/Laurel/CBMC/cbmc-bounds-check.patch"
           git apply "$STRATA/StrataTest/Backends/CBMC/cbmc-regex-support.patch"
           git apply "$STRATA/StrataTest/Backends/CBMC/cbmc-quantifier-simplify.patch"
           export CCACHE_BASEDIR=$PWD
@@ -68,5 +68,5 @@ jobs:
       - name: Run Python CBMC pipeline tests
         shell: bash
         run: |
-          pip install ./Tools/Python-base ./Tools/strata-python
+          pip install ./.lake/packages/StrataDDM/Python/strata ./Python/strata-python
           ./StrataPythonTest/run_py_cbmc_tests.sh
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index be5ce80..455e4d5 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -42,26 +42,18 @@ jobs:
         with:
           python-version: '3.14'
       - name: Build using pip
-        # `strata-base` (Tools/Python-base) and `strata-python` (Tools/strata-python)
-        # both live in this repo.
+        # `strata` (base package) comes from the StrataDDM dependency under .lake;
+        # `strata-python` lives in this repo.
         run: |
-          pip install ./Tools/Python-base
-          pip install ./Tools/strata-python
+          pip install ./.lake/packages/StrataDDM/Python/strata ./Python/strata-python
       - name: Run pyInterpret golden-file tests
         working-directory: StrataPythonTest
         shell: bash
         run: ./run_py_interpret.sh
-      - name: Run pyAnalyze SARIF tests
-        working-directory: StrataPythonTest
-        shell: bash
-        run: python run_py_analyze_sarif.py
       - name: Run pyAnalyze golden-file tests
         working-directory: StrataPythonTest
         shell: bash
         run: ./run_py_analyze.sh
-      - name: Run regex differential tests
-        working-directory: StrataPythonTest/Regex
-        run: python diff_test.py
       - name: Save lake cache
         uses: ./.github/actions/save-lake-cache
         with:
@@ -89,8 +81,7 @@ jobs:
         use-restore-keys: "false"
     - name: Build using pip
       run: |
-        pip install ./Tools/Python-base
-        pip install ./Tools/strata-python
+        pip install ./.lake/packages/StrataDDM/Python/strata ./Python/strata-python
     - name: Install Lean
       uses: leanprover/lean-action@v1
       with:
@@ -157,8 +148,7 @@ jobs:
         use-restore-keys: "false"
     - name: Build using pip
       run: |
-        pip install ./Tools/Python-base
-        pip install ./Tools/strata-python
+        pip install ./.lake/packages/StrataDDM/Python/strata ./Python/strata-python
     - name: Install Lean (for lake env)
       uses: leanprover/lean-action@v1
       with:
@@ -184,7 +174,7 @@ jobs:
       # check runs in-process inside the StrataPythonTestExtra/CpythonDiffTest
       # Lean test (driven by this script), so no separate `strata` CLI is built.
       run: FAIL_FAST=1 ./scripts/run_cpython_tests.sh ${{ matrix.python_version }}
-      working-directory: Tools/strata-python
+      working-directory: Python/strata-python
 
   cbmc:
     needs: build_and_test_lean
diff --git a/Python/strata-python/scripts/run_cpython_tests.sh b/Python/strata-python/scripts/run_cpython_tests.sh
index 2e455c7..85b7861 100755
--- a/Python/strata-python/scripts/run_cpython_tests.sh
+++ b/Python/strata-python/scripts/run_cpython_tests.sh
@@ -25,6 +25,8 @@ VER="$1"
 prefix="cpython-$VER"
 if [ -d "$prefix" ]; then
   echo "Skipping download: $prefix already exists"
+else
+  git clone https://github.com/python/cpython.git --branch "$VER" --depth 1 "$prefix"
 fi
 
 # Files in the CPython test suite that are expected to fail to parse (and so
diff --git a/StrataPythonTest/ToLaurelTest.lean b/StrataPythonTest/ToLaurelTest.lean
index 8203c98..eaa3492 100644
--- a/StrataPythonTest/ToLaurelTest.lean
+++ b/StrataPythonTest/ToLaurelTest.lean
@@ -68,6 +68,7 @@ private def fmtHighType : HighType → String
   | .TMap _ _ => "TMap"
   | .UserDefined name => s!"UserDefined({name})"
   | .Applied _ _ => "Applied"
+  | .Pure _ => "Pure"
   | .Intersection _ => "Intersection"
   | .TBv n => s!"TBv({n})"
   | .Unknown => "Unknown"
diff --git a/StrataPythonTest/CI/InterpretTests.lean b/StrataPythonTestExtra/CI/InterpretTests.lean
similarity index 100%
rename from StrataPythonTest/CI/InterpretTests.lean
rename to StrataPythonTestExtra/CI/InterpretTests.lean
diff --git a/lake-manifest.json b/lake-manifest.json
index 433741e..406a211 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "7b40c42a9f279ef6aaa9000cfd8d728476c953fa",
+   "rev": "ee0b2ecb2e6be3aaf0f69b7b29a40d96767ee6ee",
    "name": "Strata",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "fbd9f71d6f03f56d71dc0ea4c40fcca7f4ebb6f8",
+   "rev": "18c1ade5cd00b4c955d5b9f341ab70d5573f27ba",
    "name": "StrataDDM",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lakefile.toml b/lakefile.toml
index 6c8dbbe..6e6252a 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -1,7 +1,7 @@
 name = "StrataPython"
 version = "0.1.0"
 defaultTargets = ["StrataPython"]
-testDriver = "StrataTestMain"
+testDriver = "StrataPythonFrontEndTestMain"
 
 [[require]]
 name = "Strata"
@@ -10,7 +10,7 @@ rev = "main"
 
 [[input_file]]
 name = "PythonDialectIon"
-path = "Tools/strata-python/dialects/Python.dialect.st.ion"
+path = "Python/strata-python/dialects/Python.dialect.st.ion"
 text = true
 
 [[lean_lib]]
@@ -26,7 +26,7 @@ name = "StrataPythonTestExtra"
 globs = ["StrataPythonTestExtra.+"]
 
 [[lean_exe]]
-name = "StrataTestMain"
+name = "StrataPythonFrontEndTestMain"
 needs = ["StrataPython", "StrataPythonTest"]
 
 [[lean_exe]]