fix(ci): Missing edits, lake update

.github/workflows/cbmc.yml

@@ -32,7 +32,7 @@ jobs:
           git clone --depth 1 --branch cbmc-6.8.0 https://github.com/diffblue/cbmc.git cbmc-src
           cd cbmc-src
           git apply "$GITHUB_WORKSPACE/StrataTest/Backends/CBMC/cbmc-string-support.patch"
-          git apply "$GITHUB_WORKSPACE/StrataTest/Languages/Laurel/cbmc-bounds-check.patch"
+          git apply "$GITHUB_WORKSPACE/StrataTest/Languages/Laurel/CBMC/cbmc-bounds-check.patch"
           git apply "$GITHUB_WORKSPACE/StrataTest/Backends/CBMC/cbmc-regex-support.patch"
           git apply "$GITHUB_WORKSPACE/StrataTest/Backends/CBMC/cbmc-quantifier-simplify.patch"
           export CCACHE_BASEDIR=$PWD
@@ -79,4 +79,4 @@ jobs:
       - name: Run Laurel CBMC pipeline tests
         shell: bash
         run: |
-          ./StrataTest/Languages/Laurel/run_laurel_cbmc_tests.sh
+          ./StrataTest/Languages/Laurel/CBMC/run_laurel_cbmc_tests.sh

.github/workflows/ci.yml

@@ -102,10 +102,6 @@ jobs:
       actions: write
     steps:
       - uses: actions/checkout@v6
-      - name: Build API documentation package
-        uses: leanprover/lean-action@v1
-        with:
-          lake-package-directory: 'docs/api'
       - name: Restore lake cache
         uses: actions/cache/restore@v5
         with:
@@ -115,6 +111,10 @@ jobs:
           key: docs-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'docs/verso/lean-toolchain') }}-${{ hashFiles('lake-manifest.json', 'docs/verso/lake-manifest.json') }}-${{ hashFiles('**/*.st') }}-${{ github.sha }}
           restore-keys: |
             docs-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain', 'docs/verso/lean-toolchain') }}-${{ hashFiles('lake-manifest.json', 'docs/verso/lake-manifest.json') }}-${{ hashFiles('**/*.st') }}
+      - name: Build API documentation package
+        uses: leanprover/lean-action@v1
+        with:
+          lake-package-directory: 'docs/api'
       - name: Build documentation package
         uses: leanprover/lean-action@v1
         with:

Strata.lean

@@ -43,6 +43,7 @@ import Strata.Languages.Core.EntryPoint
 import Strata.Languages.Core.VerifierProofs
 import Strata.Languages.Dyn.Dyn
 import Strata.Languages.Dyn.Verify
+import Strata.Languages.GOTO
 import Strata.Languages.Laurel.FilterPrelude
 
 /- DDM -/
@@ -52,8 +53,6 @@ import StrataDDM
 import Strata.Backends.CBMC
 
 /- Dialect Library — additional (can't go in aggregates due to cycles) -/
-import Strata.DL.Imperative.CFGToCProverGOTO
-import Strata.DL.Imperative.ToCProverGOTO
 import Strata.DL.SMT.Denote
 import Strata.DL.SMT.FactoryCorrect
 import Strata.DL.SMT.Translate
@@ -99,5 +98,7 @@ import Strata.Languages.Dyn.DDMTransform.Parse
 import Strata.Languages.Dyn.DDMTransform.Translate
 import Strata.Util.Random
 
+import Strata.Examples.Embedded
+import Strata.Examples.EmbeddedData
 
 -- noimport: Strata.Util.IOTests (used for tests)

StrataTest/Languages/Laurel/CBMC/laurel_to_cbmc.sh

@@ -23,9 +23,9 @@ LAUREL="$(cd "$(dirname "$1")" && pwd)/$(basename "$1")"
 # deriveBaseName in StrataMain.lean strips .st from the filename
 BN=$(basename "$LAUREL" .st)
 
-# Locate project root (three levels up from this script's directory)
+# Locate project root (four levels up from this script's directory)
 SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)"
-PROJECT_ROOT="$(cd "$SCRIPT_DIR/../../.." && pwd)"
+PROJECT_ROOT="$(cd "$SCRIPT_DIR/../../../.." && pwd)"
 
 # Use a temporary directory for intermediate files
 WORK_DIR=$(mktemp -d)

StrataTest/Languages/Laurel/CBMC/run_laurel_cbmc_tests.sh

@@ -16,7 +16,7 @@ set -o pipefail
 
 SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)"
 TESTS_DIR="$SCRIPT_DIR/tests"
-PROJECT_ROOT="$(cd "$SCRIPT_DIR/../../.." && pwd)"
+PROJECT_ROOT="$(cd "$SCRIPT_DIR/../../../.." && pwd)"
 EXPECTED="$TESTS_DIR/cbmc_expected.txt"
 
 passed=0

docs/verso/lake-manifest.json

@@ -52,7 +52,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "fbd9f71d6f03f56d71dc0ea4c40fcca7f4ebb6f8",
+   "rev": "4ea13cd3ef6e6e0bc70629ef818155c808c47320",
    "name": "StrataDDM",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

editors/emacs/core-st-mode.el

@@ -26,8 +26,9 @@
     "Sequence.append" "Sequence.build" "Sequence.update"
     "Sequence.contains" "Sequence.take" "Sequence.drop" "str.len"
     "str.concat" "str.substr" "str.to.re" "str.in.re" "str.prefixof"
-    "str.suffixof" "re.allchar" "re.all" "re.range" "re.concat" "re.*"
-    "re.+" "re.loop" "re.union" "re.inter" "re.comp" "re.none"
+    "str.suffixof" "str.contains" "str.indexof" "str.replace" "str.at"
+    "str.lt" "str.le" "re.allchar" "re.all" "re.range" "re.concat"
+    "re.*" "re.+" "re.loop" "re.union" "re.inter" "re.comp" "re.none"
     "Int.DivT" "Int.ModT" "Int.SafeDivT" "Int.SafeModT" "Bv.SafeAdd"
     "Bv.SafeSub" "Bv.SafeMul" "Bv.SafeNeg" "Bv.SafeSDiv" "Bv.SafeSMod"
     "Bv.SNegOverflow" "Bv.UNegOverflow" "Bv.SAddOverflow"

editors/vscode/syntaxes/core-st.tmLanguage.json

@@ -84,7 +84,7 @@
       ]
     },
     "function-call": {
-      "match": "\\b(Sequence\\.empty|Sequence\\.length|Sequence\\.select|Sequence\\.append|Sequence\\.build|Sequence\\.update|Sequence\\.contains|Sequence\\.take|Sequence\\.drop|str\\.len|str\\.concat|str\\.substr|str\\.to\\.re|str\\.in\\.re|str\\.prefixof|str\\.suffixof|re\\.allchar|re\\.all|re\\.range|re\\.concat|re\\.\\*|re\\.\\+|re\\.loop|re\\.union|re\\.inter|re\\.comp|re\\.none|Int\\.DivT|Int\\.ModT|Int\\.SafeDivT|Int\\.SafeModT|Bv\\.SafeAdd|Bv\\.SafeSub|Bv\\.SafeMul|Bv\\.SafeNeg|Bv\\.SafeSDiv|Bv\\.SafeSMod|Bv\\.SNegOverflow|Bv\\.UNegOverflow|Bv\\.SAddOverflow|Bv\\.SSubOverflow|Bv\\.SMulOverflow|Bv\\.SDivOverflow|Bv\\.UAddOverflow|Bv\\.USubOverflow|Bv\\.UMulOverflow|bvconcat\\{[0-9]+\\}\\{[0-9]+\\}|bvextract\\{[0-9]+\\}\\{[0-9]+\\}\\{[0-9]+\\})\\b",
+      "match": "\\b(Sequence\\.empty|Sequence\\.length|Sequence\\.select|Sequence\\.append|Sequence\\.build|Sequence\\.update|Sequence\\.contains|Sequence\\.take|Sequence\\.drop|str\\.len|str\\.concat|str\\.substr|str\\.to\\.re|str\\.in\\.re|str\\.prefixof|str\\.suffixof|str\\.contains|str\\.indexof|str\\.replace|str\\.at|str\\.lt|str\\.le|re\\.allchar|re\\.all|re\\.range|re\\.concat|re\\.\\*|re\\.\\+|re\\.loop|re\\.union|re\\.inter|re\\.comp|re\\.none|Int\\.DivT|Int\\.ModT|Int\\.SafeDivT|Int\\.SafeModT|Bv\\.SafeAdd|Bv\\.SafeSub|Bv\\.SafeMul|Bv\\.SafeNeg|Bv\\.SafeSDiv|Bv\\.SafeSMod|Bv\\.SNegOverflow|Bv\\.UNegOverflow|Bv\\.SAddOverflow|Bv\\.SSubOverflow|Bv\\.SMulOverflow|Bv\\.SDivOverflow|Bv\\.UAddOverflow|Bv\\.USubOverflow|Bv\\.UMulOverflow|bvconcat\\{[0-9]+\\}\\{[0-9]+\\}|bvextract\\{[0-9]+\\}\\{[0-9]+\\}\\{[0-9]+\\})\\b",
       "captures": {
         "1": { "name": "support.function.builtin.core-st" }
       }

lake-manifest.json

@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "fbd9f71d6f03f56d71dc0ea4c40fcca7f4ebb6f8",
+   "rev": "4ea13cd3ef6e6e0bc70629ef818155c808c47320",
    "name": "StrataDDM",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lakefile.toml

@@ -4,6 +4,9 @@ defaultTargets = ["Strata", "StrataToCBMC", "StrataCoreToGoto"]
 testDriver = "StrataTestMain"
 lintDriver = "CheckImports"
 
+[leanOptions]
+warningAsError = true
+
 [[require]]
 name = "StrataDDM"
 git = "https://github.com/strata-org/Strata-DDM"
@@ -49,3 +52,6 @@ root = "Scripts.CheckImports"
 name = "ImportStats"
 root = "Scripts.ImportStats"
 
+[[lean_exe]]
+name = "GenerateEmbedded"
+root = "Scripts.GenerateEmbedded"