feat: structured-to-unstructured forward soundness for simple-shape programs (small-step)

.kiro/steering/structure.md

@@ -15,8 +15,6 @@ Strata is a Lean4 verification framework using **dialects** as composable langua
 - `Strata/` - Core implementation (DDM, dialects, languages, transforms, backends)
 - `StrataTest/` - Unit tests (mirrors Strata/ structure)
 - `Examples/` - Sample programs (`.st` files, naming: `<name>.<dialect>.st`)
-- `Tools/` - External tools (BoogieToStrata, Python utilities)
-- `vcs/` - Generated SMT2 verification conditions
 
 ### Core Components
 
@@ -34,9 +32,7 @@ Strata is a Lean4 verification framework using **dialects** as composable langua
 - `Core/` - Primary verification language (procedures, contracts, VCG, SMT encoding)
 - `C_Simp/` - Simplified C-like language
 - `Dyn/` - Dynamic language example
-- `Laurel/` - A common representation for front-end languages like Java, Python and JavaScript.
-Translated to Core.
-- `Python/` - The well-known Python language
+- `Laurel/` - A common representation for front-end languages like Java, Python and JavaScript. Translated to Core.
 
 **`Strata/Transform/`** - Program Transformations
 - Each transformation has implementation + optional correctness proof (`*Correct.lean`)

README.md

@@ -28,13 +28,10 @@ changes!**
    (`cvc5` and `z3`). See [Installing dependencies → SMT Solvers](#smt-solvers)
    below.
 
-3. **Python 3.11+**: required for Python-related tests and the `strata`
-   Python tooling. See [Installing dependencies → Python](#python) below.
-
-4. **Java JDK (11 or later)**: required for Java code generation tests.
+3. **Java JDK (11 or later)**: required for Java code generation tests.
    See [Installing dependencies → Java](#java-for-code-generation-tests) below.
 
-5. **ion-java jar (1.11.11)**: required for the Java/Ion integration test.
+4. **ion-java jar (1.11.11)**: required for the Java/Ion integration test.
    See [Installing dependencies → Java](#java-for-code-generation-tests) below.
 
 ### Installing dependencies
@@ -54,18 +51,6 @@ cp /path/to/cvc5 /path/to/z3 ~/.local/bin/
 # or: sudo cp /path/to/cvc5 /path/to/z3 /usr/local/bin/
 ```
 
-#### Python
-
-Python 3.11 or later is required. Install the `strata` Python package inside a
-virtual environment (recommended; avoids PEP 668's `externally-managed-environment`
-error on Debian/Ubuntu 23.04+):
-
-```bash
-python3 -m venv .venv
-source .venv/bin/activate
-pip install ./Tools/Python
-```
-
 #### Java (for code generation tests)
 
 A JDK (11+) providing `javac` must be on your `PATH`. For running the
@@ -81,7 +66,6 @@ wget -q -O StrataTestExtra/Languages/Java/testdata/ion-java-1.11.11.jar \
 ```bash
 cvc5 --version    # should print version info
 z3 --version      # should print version info
-python3 --version # should be 3.11+
 ```
 
 ## Build
@@ -111,13 +95,10 @@ Two kinds of tests coexist in this repo:
   These accept prefix filters:
 
 ```bash
-# Run all extra tests except Python (which requires the Python package)
-lake test -- --exclude Languages.Python
-
-# Run only Python extra tests (requires `pip install ./Tools/Python`)
-lake test -- Languages.Python
+# Run all extra tests except those in the Imperative namespace
+lake test -- --exclude DL.Imperative
 
-# Run all extra tests (Python tests will fail without the Python package above)
+# Run all extra tests
 lake test
 ```
 

Scripts/JavaGenTestData.lean

@@ -0,0 +1,79 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+import StrataDDM
+
+/-!
+# Java test data generation helper
+
+Usage:
+  lake env lean --run Scripts/JavaGenTestData.lean javaGen <dialect-file> <package> <output-dir>
+  lake env lean --run Scripts/JavaGenTestData.lean print --include <dir> <file>
+
+Note: Unlike the former CLI `javaGen` command, this script only loads dialects
+from files — it does not support referencing preloaded dialect names directly.
+This is sufficient for the testdata regeneration workflow.
+-/
+
+open StrataDDM
+
+def javaGen (dialectPath packageName outputDir : String) : IO Unit := do
+  let fm ← mkDialectFileMap
+  let d ← readStrataDialectFile fm dialectPath
+  match StrataDDM.Java.generateDialect d packageName with
+  | .ok files =>
+    StrataDDM.Java.writeJavaFiles outputDir packageName files
+    IO.println s!"Generated Java files for {d.name} in {outputDir}/{StrataDDM.Java.packageToPath packageName}"
+  | .error msg =>
+    IO.eprintln s!"Error generating Java: {msg}"
+    IO.Process.exit 1
+
+def printFile (includeDirs : List String) (file : String) : IO Unit := do
+  let fm ← mkDialectFileMap
+  let mut fm := fm
+  for dir in includeDirs do
+    match ← fm.addSearchPath dir |>.toBaseIO with
+    | .error msg =>
+      IO.eprintln msg
+      IO.Process.exit 1
+    | .ok fm' => fm := fm'
+  let ld ← fm.getLoaded
+  if mem : file ∈ ld.dialects then
+    IO.print <| ld.dialects.format file mem
+    return
+  match ← readStrataFile fm file with
+  | .dialect d =>
+    let ld ← fm.getLoaded
+    if mem : d.name ∈ ld.dialects then
+      IO.print <| ld.dialects.format d.name mem
+    else
+      IO.eprintln "Internal error reading file."
+      IO.Process.exit 1
+  | .program pgm =>
+    IO.print <| toString pgm
+
+private def parseIncludeArgs (args : List String) : List String × List String :=
+  go args []
+where
+  go : List String → List String → List String × List String
+    | "--include" :: dir :: rest, includes => go rest (dir :: includes)
+    | other, includes => (includes.reverse, other)
+
+def main (args : List String) : IO Unit := do
+  match args with
+  | "javaGen" :: dialectPath :: packageName :: outputDir :: _ =>
+    javaGen dialectPath packageName outputDir
+  | "print" :: rest =>
+    let (includeDirs, fileArgs) := parseIncludeArgs rest
+    match fileArgs with
+    | [file] => printFile includeDirs file
+    | _ =>
+      IO.eprintln "Usage: ... print [--include <dir>]... <file>"
+      IO.Process.exit 1
+  | _ =>
+    IO.eprintln "Usage:"
+    IO.eprintln "  lake env lean --run Scripts/JavaGenTestData.lean javaGen <dialect> <package> <output-dir>"
+    IO.eprintln "  lake env lean --run Scripts/JavaGenTestData.lean print [--include <dir>]... <file>"
+    IO.Process.exit 1

Scripts/LaurelToCBMC.lean

@@ -0,0 +1,134 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+import Strata.Backends.CBMC.GOTO.CoreToGOTOPipeline
+import Strata.Languages.Laurel
+
+/-! # LaurelToCBMC
+
+Script that replaces `laurel_to_cbmc.sh`. Translates a Laurel `.lr.st` source
+file through the full Strata pipeline to CBMC verification:
+
+1. Parse Laurel source → Laurel AST
+2. Translate Laurel → Core
+3. Inline procedures, type-check, generate CProver GOTO JSON
+4. Invoke `symtab2gb` to produce a GOTO binary
+5. Invoke `goto-cc` to add C scaffolding
+6. Invoke `goto-instrument --dfcc` for contract instrumentation
+7. Invoke `cbmc` for bounded model checking
+
+Usage:
+  lake env lean --run Scripts/LaurelToCBMC.lean <file.lr.st>
+
+Environment variables:
+  CBMC              - path to cbmc binary (default: cbmc)
+  GOTO_CC           - path to goto-cc binary (default: goto-cc)
+  GOTO_INSTRUMENT   - path to goto-instrument binary (default: goto-instrument)
+-/
+
+open Strata
+
+/-- Strip well-known Strata file suffixes from a file path's basename. -/
+private def deriveBaseName (file : String) : String :=
+  let name := System.FilePath.fileName file |>.getD file
+  let suffixes := [".lr.st", ".laurel.st", ".st"]
+  match suffixes.find? (name.endsWith ·) with
+  | some sfx => (name.dropEnd sfx.length).toString
+  | none     => name
+
+/-- Read an environment variable, returning a default if unset or empty. -/
+private def getEnvOrDefault (var : String) (default : String) : IO String := do
+  match ← IO.getEnv var with
+  | some v => if v.isEmpty then pure default else pure v
+  | none   => pure default
+
+/-- Run an external process. Prints stdout/stderr to the caller's streams and
+    returns the exit code. -/
+private def runProcess (step : String) (cmd : String) (args : Array String) : IO UInt32 := do
+  let proc ← IO.Process.spawn {
+    cmd := cmd
+    args := args
+    stdout := .inherit
+    stderr := .inherit
+    stdin := .inherit
+  }
+  let exitCode ← proc.wait
+  if exitCode != 0 then
+    IO.eprintln s!"Error: {step} failed (exit code {exitCode})"
+  return exitCode
+
+/-- The Laurel-to-GOTO translation pipeline. Parses a Laurel source file,
+    translates to Core, inlines procedures, type-checks, and emits CProver GOTO
+    JSON files (`<baseName>.symtab.json` and `<baseName>.goto.json`) in the
+    given output directory. -/
+private def laurelAnalyzeToGoto (path : System.FilePath) (outputDir : System.FilePath)
+    (baseName : String) : IO Unit := do
+  let content ← IO.FS.readFile path
+  let laurelProgram ← Strata.parseLaurelText path content
+  match ← Strata.Laurel.translate {} laurelProgram with
+  | (none, diags) =>
+    throw (IO.userError s!"Core translation errors: {diags.map (·.message)}")
+  | (some coreProgram, _) =>
+    -- Use the output directory as a prefix so files land in tmpDir
+    let outputBaseName := (outputDir / baseName).toString
+    match ← Strata.inlineCoreToGotoFiles coreProgram outputBaseName
+              (sourceText := some content) |>.toBaseIO with
+    | .ok () => pure ()
+    | .error msg => throw (IO.userError msg)
+
+def main (args : List String) : IO UInt32 := do
+  match args with
+  | [file] =>
+    unless file.endsWith ".lr.st" || file.endsWith ".laurel.st" do
+      IO.eprintln s!"Error: expected a .lr.st file, got: {file}"
+      return 1
+    let path : System.FilePath := file
+    unless ← path.pathExists do
+      IO.eprintln s!"Error: file not found: {file}"
+      return 1
+    let baseName := deriveBaseName file
+
+    -- Use a temporary directory for intermediate files (cleaned up automatically)
+    IO.FS.withTempDir fun tmpDir => do
+
+    -- Step 1: Laurel → GOTO JSON (in tmp dir)
+    let result ← (laurelAnalyzeToGoto path tmpDir baseName).toBaseIO
+    match result with
+    | .error e =>
+      IO.eprintln s!"Error: {e}"
+      return 1
+    | .ok () => pure ()
+
+    let symTabFile := (tmpDir / s!"{baseName}.symtab.json").toString
+    let gotoFile := (tmpDir / s!"{baseName}.goto.json").toString
+    let gbFile := (tmpDir / s!"{baseName}.gb").toString
+    let ccGbFile := (tmpDir / s!"{baseName}_cc.gb").toString
+    let dfccGbFile := (tmpDir / s!"{baseName}_dfcc.gb").toString
+
+    -- Step 2: symtab2gb
+    let rc ← runProcess "symtab2gb" "symtab2gb"
+      #[symTabFile, "--goto-functions", gotoFile, "--out", gbFile]
+    if rc != 0 then return rc
+
+    -- Step 3: goto-cc (add C scaffolding)
+    let gotoCC ← getEnvOrDefault "GOTO_CC" "goto-cc"
+    let rc ← runProcess "goto-cc" gotoCC
+      #["--function", "main", "-o", ccGbFile, gbFile]
+    if rc != 0 then return rc
+
+    -- Step 4: goto-instrument --dfcc
+    let gotoInstrument ← getEnvOrDefault "GOTO_INSTRUMENT" "goto-instrument"
+    let rc ← runProcess "goto-instrument --dfcc" gotoInstrument
+      #["--dfcc", "main", ccGbFile, dfccGbFile]
+    if rc != 0 then return rc
+
+    -- Step 5: cbmc verification
+    let cbmc ← getEnvOrDefault "CBMC" "cbmc"
+    runProcess "cbmc" cbmc
+      #[dfccGbFile, "--function", "main", "--z3", "--verbosity", "9"]
+
+  | _ =>
+    IO.eprintln "Usage: LaurelToCBMC <file.lr.st>"
+    return 1

Strata.lean

@@ -34,6 +34,7 @@ import Strata.Transform.CallElimCorrect
 import Strata.Transform.CoreSpecification
 import Strata.Transform.DetToKleeneCorrect
 import Strata.Transform.ProcBodyVerifyCorrect
+import Strata.Transform.StructuredToUnstructuredCorrect
 
 /- Strata Languages — additional -/
 import Strata.Languages.B3