From beca58b66419faa5edc560a0db61a9abf29c8889 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 18 Mar 2026 15:17:43 +0100
Subject: [PATCH 1/3] Rewrite StrataCoreToGoto for multi-procedure programs
 with contracts

- Iterate over all procedures and functions in the Core program
- Apply call elimination to inline contracts (configurable via --no-call-elim)
- Re-type-check after call elimination for new variable discovery
- Seed type environment with global variable types
- Apply GOTO pipeline passes: function inlining, recursive inlining,
  datatype partial evaluation, datatype axiom/recursive function axiom
  generation, datatype expression rewriting
- Deduplicate symbol table, add default symbols

Tests:
- test_multi_proc.core.st: multi-procedure Core program with contracts
- test_strata_core_to_goto.sh: verifies translation, symbol table,
  contract annotations, and GOTO assertions

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 StrataCoreToGoto.lean                         | 159 ++++++++++++++++--
 .../CBMC/GOTO/test_multi_proc.core.st         |  23 +++
 .../CBMC/GOTO/test_strata_core_to_goto.sh     |  75 +++++++++
 3 files changed, 241 insertions(+), 16 deletions(-)
 create mode 100644 StrataTest/Backends/CBMC/GOTO/test_multi_proc.core.st
 create mode 100755 StrataTest/Backends/CBMC/GOTO/test_strata_core_to_goto.sh

diff --git a/StrataCoreToGoto.lean b/StrataCoreToGoto.lean
index 0aa2ac279..5fac6924c 100644
--- a/StrataCoreToGoto.lean
+++ b/StrataCoreToGoto.lean
@@ -4,8 +4,11 @@
   SPDX-License-Identifier: Apache-2.0 OR MIT
 -/
 
-import Strata.Backends.CBMC.GOTO.CoreToCProverGOTO
+import Strata.Backends.CBMC.GOTO.CoreToGOTOPipeline
+import Strata.Backends.CBMC.GOTO.DefaultSymbols
+import Strata.Backends.CBMC.CollectSymbols
 import Strata.Languages.Core.Verifier
+import Strata.Transform.CallElim
 import Strata.Util.IO
 
 open Strata
@@ -18,11 +21,13 @@ def usageMessage : Std.Format :=
   Options:{Std.Format.line}\
   {Std.Format.line}  \
   --output-dir <dir>    Directory for output files (default: current directory){Std.Format.line}  \
-  --program-name <name> Program name for GOTO output (default: derived from filename)"
+  --program-name <name> Program name for GOTO output (default: derived from filename){Std.Format.line}  \
+  --no-call-elim        Skip call elimination (keep raw calls for external DFCC)"
 
 structure GotoOptions where
   outputDir : String := "."
   programName : Option String := none
+  callElim : Bool := true
 
 def parseOptions (args : List String) : Except Std.Format (GotoOptions × String) :=
   go {} args
@@ -30,13 +35,13 @@ def parseOptions (args : List String) : Except Std.Format (GotoOptions × String
     go : GotoOptions → List String → Except Std.Format (GotoOptions × String)
     | opts, "--output-dir" :: dir :: rest => go {opts with outputDir := dir} rest
     | opts, "--program-name" :: name :: rest => go {opts with programName := some name} rest
+    | opts, "--no-call-elim" :: rest => go {opts with callElim := false} rest
     | opts, [file] => .ok (opts, file)
     | _, [] => .error "StrataCoreToGoto requires a .core.st file as input"
     | _, args => .error f!"Unknown options: {args}"
 
 def deriveBaseName (file : String) : String :=
   let name := System.FilePath.fileName file |>.getD file
-  -- Strip .core.st or .st suffix
   if name.endsWith ".core.st" then (name.dropEnd 8).toString
   else if name.endsWith ".st" then (name.dropEnd 3).toString
   else name
@@ -50,32 +55,154 @@ def main (args : List String) : IO UInt32 := do
       return 1
     let baseName := deriveBaseName file
     let programName := opts.programName.getD baseName
-    if programName.any "/" || programName.any ".." then
-      IO.println "Error: --program-name must be a simple filename without path separators"
-      return 1
     let dir := System.FilePath.mk opts.outputDir
     IO.FS.createDirAll dir
+
     let text ← Strata.Util.readInputSource file
     let inputCtx := Lean.Parser.mkInputContext text (Strata.Util.displayName file)
     let dctx := Elab.LoadedDialects.builtin
     let dctx := dctx.addDialect! Core
     let leanEnv ← Lean.mkEmptyEnvironment 0
     match Strata.Elab.elabProgram dctx leanEnv inputCtx with
-    | .ok pgm =>
-      let symTabFile := dir / s!"{programName}.symtab.json"
-      let gotoFile := dir / s!"{programName}.goto.json"
-      CoreToGOTO.writeToGotoJson
-        (programName := programName)
-        (symTabFileName := symTabFile.toString)
-        (gotoFileName := gotoFile.toString)
-        pgm
-      IO.println s!"Written {symTabFile} and {gotoFile}"
-      return 0
     | .error errors =>
       for e in errors do
         let msg ← e.toString
         IO.println s!"Error: {msg}"
       return 1
+    | .ok pgm =>
+      -- Type check (translates DDM Program → Core.Program)
+      let Ctx := { Lambda.LContext.default with
+        functions := Core.Factory, knownTypes := Core.KnownTypes }
+      let Env := Lambda.TEnv.default
+      let tcPgm ← match Strata.typeCheck inputCtx pgm with
+        | .ok p => pure p
+        | .error e => IO.println s!"Type check error: {e.message}"; return 1
+      IO.println "[Strata.Core] Type Checking Succeeded!"
+
+      -- Apply call elimination to inline contracts (assert requires / assume ensures)
+      let tcPgm ← if opts.callElim then
+        match Core.Transform.run tcPgm (fun p => do
+              let (_, p) ← Core.CallElim.callElim' p; return p) with
+        | .ok p => pure p
+        | .error e => IO.println s!"Call elimination error: {e}"; return 1
+      else pure tcPgm
+
+      -- Re-type-check after call elimination (discovers new variables)
+      let tcPgm ← match Core.typeCheck .default tcPgm with
+        | .ok p => pure p
+        | .error e => IO.println s!"Re-type-check error: {e}"; return 1
+
+      -- Apply GOTO pipeline passes
+      let tcPgm := inlineFuncDefsInProgram tcPgm
+      let tcPgm := inlineRecFuncDefsInProgram tcPgm
+      let tcPgm := partialEvalDatatypesInProgram tcPgm
+
+      -- Collect procedures and functions
+      let procs := tcPgm.decls.filterMap fun d => d.getProc?
+      let funcs := tcPgm.decls.filterMap fun d =>
+        match d.getFunc? with
+        | some f =>
+          let name := Core.CoreIdent.toPretty f.name
+          if f.body.isSome && f.typeArgs.isEmpty
+            && name != "Int.DivT" && name != "Int.ModT"
+          then some f else none
+        | none => none
+
+      if procs.isEmpty && funcs.isEmpty then
+        IO.println "Error: No procedures or functions found"
+        return 1
+
+      -- Collect axioms and type symbols
+      let axioms := tcPgm.decls.filterMap fun d => d.getAxiom?
+      let dtAxioms := generateDatatypeAxioms tcPgm
+      let recAxioms := generateRecFuncAxioms tcPgm (unrollDepth := 0)
+      let axioms := axioms ++ dtAxioms ++ recAxioms
+      let distincts := tcPgm.decls.filterMap fun d => match d with
+        | .distinct name es _ => some (name, es) | _ => none
+      let typeSyms ← match collectExtraSymbols tcPgm with
+        | .ok s => pure s
+        | .error e => IO.println s!"Error collecting symbols: {e}"; return 1
+      let gotoDtInfo := collectGotoDatatypeInfo tcPgm
+
+      -- Translate each procedure and function to GOTO
+      let mut symtabPairs : List (String × Lean.Json) := []
+      let mut gotoFns : Array Lean.Json := #[]
+      -- Seed type environment with global variable types
+      let globalVarEntries : Map Core.Expression.Ident Core.Expression.Ty :=
+        tcPgm.decls.filterMap fun d =>
+          match d with
+          | .var name ty _ _ => some (name, ty)
+          | _ => none
+      let Env := Lambda.TEnv.addInNewestContext
+        (T := ⟨Core.ExpressionMetadata, Unit⟩) Env globalVarEntries
+
+      let mut allLiftedFuncs : List Core.Function := []
+
+      for p in procs do
+        let procName := Core.CoreIdent.toPretty p.header.name
+        match procedureToGotoCtx Env p (axioms := axioms) (distincts := distincts)
+              (varTypes := tcPgm.getVarTy?) with
+        | .error e => IO.println s!"Warning: skipping procedure {procName}: {e}"
+        | .ok (ctx, liftedFuncs) =>
+          allLiftedFuncs := allLiftedFuncs ++ liftedFuncs
+          let ctx := rewriteDatatypeExprsInCtx gotoDtInfo ctx
+          let ctx ← lowerAddressOfInCtx ctx
+          let json ← IO.ofExcept (CoreToGOTO.CProverGOTO.Context.toJson procName ctx)
+          match json.symtab with
+          | .obj m => symtabPairs := symtabPairs ++ m.toList
+          | _ => pure ()
+          match json.goto with
+          | .obj m =>
+            match m.toList.find? (·.1 == "functions") with
+            | some (_, .arr fns) => gotoFns := gotoFns ++ fns
+            | _ => pure ()
+          | _ => pure ()
+
+      for f in funcs ++ allLiftedFuncs do
+        let funcName := Core.CoreIdent.toPretty f.name
+        match functionToGotoCtx Env f with
+        | .error e => IO.println s!"Warning: skipping function {funcName}: {e}"
+        | .ok ctx =>
+          let json ← IO.ofExcept (CoreToGOTO.CProverGOTO.Context.toJson funcName ctx)
+          match json.symtab with
+          | .obj m => symtabPairs := symtabPairs ++ m.toList
+          | _ => pure ()
+          match json.goto with
+          | .obj m =>
+            match m.toList.find? (·.1 == "functions") with
+            | some (_, .arr fns) => gotoFns := gotoFns ++ fns
+            | _ => pure ()
+          | _ => pure ()
+
+      -- Add type symbols
+      match Lean.toJson typeSyms with
+      | .obj m => symtabPairs := symtabPairs ++ m.toList
+      | _ => pure ()
+
+      -- Deduplicate symbol table
+      let mut seen : Std.HashSet String := {}
+      let mut dedupPairs : List (String × Lean.Json) := []
+      for (k, v) in symtabPairs do
+        if !seen.contains k then
+          seen := seen.insert k
+          dedupPairs := dedupPairs ++ [(k, v)]
+
+      -- Add CBMC default symbols
+      for (k, v) in CProverGOTO.defaultSymbols (moduleName := programName) do
+        if !seen.contains k then
+          seen := seen.insert k
+          dedupPairs := dedupPairs ++ [(k, Lean.toJson v)]
+
+      let symtab := Lean.Json.mkObj [("symbolTable", Lean.Json.mkObj dedupPairs)]
+      let goto := Lean.Json.mkObj [("functions", Lean.Json.arr gotoFns)]
+
+      let symTabFile := dir / s!"{programName}.symtab.json"
+      let gotoFile := dir / s!"{programName}.goto.json"
+      IO.FS.writeFile symTabFile symtab.pretty
+      IO.FS.writeFile gotoFile goto.pretty
+      IO.println s!"Translated {procs.length} procedures and {funcs.length} functions"
+      IO.println s!"Written {symTabFile} and {gotoFile}"
+      return 0
   | .error msg =>
     IO.println f!"{msg}"
     IO.println f!"{usageMessage}"
diff --git a/StrataTest/Backends/CBMC/GOTO/test_multi_proc.core.st b/StrataTest/Backends/CBMC/GOTO/test_multi_proc.core.st
new file mode 100644
index 000000000..5629e70fe
--- /dev/null
+++ b/StrataTest/Backends/CBMC/GOTO/test_multi_proc.core.st
@@ -0,0 +1,23 @@
+program Core;
+
+var g : int;
+
+procedure helper(x : int) returns (r : int)
+spec {
+  ensures (r > x);
+  modifies g;
+}
+{
+  g := x;
+  r := x + 1;
+};
+
+procedure checker(a : int) returns (result : int)
+spec {
+  requires (a > 0);
+  ensures (result > a);
+}
+{
+  result := a + 1;
+  assert (result > a);
+};
diff --git a/StrataTest/Backends/CBMC/GOTO/test_strata_core_to_goto.sh b/StrataTest/Backends/CBMC/GOTO/test_strata_core_to_goto.sh
new file mode 100755
index 000000000..07500cbd6
--- /dev/null
+++ b/StrataTest/Backends/CBMC/GOTO/test_strata_core_to_goto.sh
@@ -0,0 +1,75 @@
+#!/bin/bash
+# Test: StrataCoreToGoto translates multi-procedure programs with contracts.
+#
+# Exercises:
+# 1. Multi-procedure translation (two procedures)
+# 2. Global variable in symbol table
+# 3. Contract annotations on procedures
+# 4. Assertions in GOTO output
+
+set -eo pipefail
+
+SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)"
+PROJECT_ROOT="$(cd "$SCRIPT_DIR/../../../.." && pwd)"
+STRATA_CORE_TO_GOTO="$PROJECT_ROOT/.lake/build/bin/StrataCoreToGoto"
+PYTHON=${PYTHON:-python3}
+
+WORK=$(mktemp -d)
+trap 'rm -rf "$WORK"' EXIT
+
+INPUT="$SCRIPT_DIR/test_multi_proc.core.st"
+
+# Test 1: Multi-procedure translation succeeds
+echo "Test 1: Multi-procedure translation"
+"$STRATA_CORE_TO_GOTO" --output-dir "$WORK" "$INPUT" 2>&1 | grep -q "Translated 2 procedures"
+echo "  OK: translated 2 procedures"
+
+# Test 2: Both procedures in symbol table
+"$PYTHON" -c "
+import json, sys
+with open('$WORK/test_multi_proc.symtab.json') as f:
+    st = json.load(f)['symbolTable']
+assert 'helper' in st, 'helper not in symtab'
+assert 'checker' in st, 'checker not in symtab'
+print('  OK: helper and checker in symbol table')
+"
+
+# Test 3: Global variable in symbol table
+"$PYTHON" -c "
+import json
+with open('$WORK/test_multi_proc.symtab.json') as f:
+    st = json.load(f)['symbolTable']
+assert 'g' in st, 'global variable g not in symtab'
+print('  OK: global variable g in symbol table')
+"
+
+# Test 4: Contract annotations present
+"$PYTHON" -c "
+import json
+with open('$WORK/test_multi_proc.symtab.json') as f:
+    st = json.load(f)['symbolTable']
+helper_type = json.dumps(st['helper']['type'])
+assert '#spec_ensures' in helper_type, 'No ensures on helper'
+assert '#spec_assigns' in helper_type, 'No assigns on helper'
+checker_type = json.dumps(st['checker']['type'])
+assert '#spec_requires' in checker_type, 'No requires on checker'
+print('  OK: contract annotations present')
+"
+
+# Test 5: GOTO output has assertions
+"$PYTHON" -c "
+import json
+with open('$WORK/test_multi_proc.goto.json') as f:
+    data = json.load(f)
+fn_names = [fn['name'] for fn in data['functions']]
+assert 'helper' in fn_names, f'helper not in goto functions: {fn_names}'
+assert 'checker' in fn_names, f'checker not in goto functions: {fn_names}'
+for fn in data['functions']:
+    if fn['name'] == 'checker':
+        types = [i['instructionId'] for i in fn['instructions']]
+        assert 'ASSERT' in types, f'No ASSERT in checker: {types}'
+        print('  OK: checker has ASSERT instruction')
+        break
+"
+
+echo "PASS: all StrataCoreToGoto tests passed"

From b00d46486e094ec2b2ebc97416aed7d0454be054 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 27 Mar 2026 23:00:31 +0000
Subject: [PATCH 2/3] Address PR review feedback from Copilot

- Sanitize programName to prevent path traversal in output filenames
- Remove unused Ctx variable
- Use Array instead of List for symtabPairs to avoid quadratic append
- Track translation errors and return non-zero exit code on failure
- Use HashMap for symbol table dedup with last-wins semantics so that
  collectExtraSymbols globals/datatypes override per-procedure entries
- Strengthen test to verify global variable has isStaticLifetime attribute
- Use set -euo pipefail in test script for consistency

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 StrataCoreToGoto.lean                         | 47 +++++++++++--------
 .../CBMC/GOTO/test_strata_core_to_goto.sh     |  7 +--
 2 files changed, 31 insertions(+), 23 deletions(-)

diff --git a/StrataCoreToGoto.lean b/StrataCoreToGoto.lean
index 5fac6924c..02bae518a 100644
--- a/StrataCoreToGoto.lean
+++ b/StrataCoreToGoto.lean
@@ -46,6 +46,11 @@ def deriveBaseName (file : String) : String :=
   else if name.endsWith ".st" then (name.dropEnd 3).toString
   else name
 
+/-- Sanitize a program name to prevent path traversal in output filenames. -/
+def sanitizeProgramName (name : String) : Option String :=
+  let s := name.replace "/" "" |>.replace "\\" "" |>.replace ".." ""
+  if s.isEmpty then none else some s
+
 def main (args : List String) : IO UInt32 := do
   match parseOptions args with
   | .ok (opts, file) =>
@@ -54,7 +59,9 @@ def main (args : List String) : IO UInt32 := do
       IO.println f!"{usageMessage}"
       return 1
     let baseName := deriveBaseName file
-    let programName := opts.programName.getD baseName
+    let programName ← match sanitizeProgramName (opts.programName.getD baseName) with
+      | some n => pure n
+      | none => IO.println "Error: invalid program name"; return 1
     let dir := System.FilePath.mk opts.outputDir
     IO.FS.createDirAll dir
 
@@ -71,8 +78,6 @@ def main (args : List String) : IO UInt32 := do
       return 1
     | .ok pgm =>
       -- Type check (translates DDM Program → Core.Program)
-      let Ctx := { Lambda.LContext.default with
-        functions := Core.Factory, knownTypes := Core.KnownTypes }
       let Env := Lambda.TEnv.default
       let tcPgm ← match Strata.typeCheck inputCtx pgm with
         | .ok p => pure p
@@ -125,8 +130,9 @@ def main (args : List String) : IO UInt32 := do
       let gotoDtInfo := collectGotoDatatypeInfo tcPgm
 
       -- Translate each procedure and function to GOTO
-      let mut symtabPairs : List (String × Lean.Json) := []
+      let mut symtabPairs : Array (String × Lean.Json) := #[]
       let mut gotoFns : Array Lean.Json := #[]
+      let mut errors : Nat := 0
       -- Seed type environment with global variable types
       let globalVarEntries : Map Core.Expression.Ident Core.Expression.Ty :=
         tcPgm.decls.filterMap fun d =>
@@ -142,14 +148,14 @@ def main (args : List String) : IO UInt32 := do
         let procName := Core.CoreIdent.toPretty p.header.name
         match procedureToGotoCtx Env p (axioms := axioms) (distincts := distincts)
               (varTypes := tcPgm.getVarTy?) with
-        | .error e => IO.println s!"Warning: skipping procedure {procName}: {e}"
+        | .error e => IO.println s!"Error: skipping procedure {procName}: {e}"; errors := errors + 1
         | .ok (ctx, liftedFuncs) =>
           allLiftedFuncs := allLiftedFuncs ++ liftedFuncs
           let ctx := rewriteDatatypeExprsInCtx gotoDtInfo ctx
           let ctx ← lowerAddressOfInCtx ctx
           let json ← IO.ofExcept (CoreToGOTO.CProverGOTO.Context.toJson procName ctx)
           match json.symtab with
-          | .obj m => symtabPairs := symtabPairs ++ m.toList
+          | .obj m => symtabPairs := symtabPairs ++ m.toList.toArray
           | _ => pure ()
           match json.goto with
           | .obj m =>
@@ -161,11 +167,11 @@ def main (args : List String) : IO UInt32 := do
       for f in funcs ++ allLiftedFuncs do
         let funcName := Core.CoreIdent.toPretty f.name
         match functionToGotoCtx Env f with
-        | .error e => IO.println s!"Warning: skipping function {funcName}: {e}"
+        | .error e => IO.println s!"Error: skipping function {funcName}: {e}"; errors := errors + 1
         | .ok ctx =>
           let json ← IO.ofExcept (CoreToGOTO.CProverGOTO.Context.toJson funcName ctx)
           match json.symtab with
-          | .obj m => symtabPairs := symtabPairs ++ m.toList
+          | .obj m => symtabPairs := symtabPairs ++ m.toList.toArray
           | _ => pure ()
           match json.goto with
           | .obj m =>
@@ -174,26 +180,27 @@ def main (args : List String) : IO UInt32 := do
             | _ => pure ()
           | _ => pure ()
 
+      if errors > 0 then
+        IO.println s!"Error: {errors} procedure/function translation(s) failed"
+        return 1
+
       -- Add type symbols
       match Lean.toJson typeSyms with
-      | .obj m => symtabPairs := symtabPairs ++ m.toList
+      | .obj m => symtabPairs := symtabPairs ++ m.toList.toArray
       | _ => pure ()
 
-      -- Deduplicate symbol table
-      let mut seen : Std.HashSet String := {}
-      let mut dedupPairs : List (String × Lean.Json) := []
+      -- Deduplicate symbol table (later entries override earlier ones so that
+      -- collectExtraSymbols globals/datatypes take precedence)
+      let mut symtabMap : Std.HashMap String Lean.Json := {}
       for (k, v) in symtabPairs do
-        if !seen.contains k then
-          seen := seen.insert k
-          dedupPairs := dedupPairs ++ [(k, v)]
+        symtabMap := symtabMap.insert k v
 
-      -- Add CBMC default symbols
+      -- Add CBMC default symbols only if not already present
       for (k, v) in CProverGOTO.defaultSymbols (moduleName := programName) do
-        if !seen.contains k then
-          seen := seen.insert k
-          dedupPairs := dedupPairs ++ [(k, Lean.toJson v)]
+        if !symtabMap.contains k then
+          symtabMap := symtabMap.insert k (Lean.toJson v)
 
-      let symtab := Lean.Json.mkObj [("symbolTable", Lean.Json.mkObj dedupPairs)]
+      let symtab := Lean.Json.mkObj [("symbolTable", Lean.Json.mkObj symtabMap.toList)]
       let goto := Lean.Json.mkObj [("functions", Lean.Json.arr gotoFns)]
 
       let symTabFile := dir / s!"{programName}.symtab.json"
diff --git a/StrataTest/Backends/CBMC/GOTO/test_strata_core_to_goto.sh b/StrataTest/Backends/CBMC/GOTO/test_strata_core_to_goto.sh
index 07500cbd6..bd15209c8 100755
--- a/StrataTest/Backends/CBMC/GOTO/test_strata_core_to_goto.sh
+++ b/StrataTest/Backends/CBMC/GOTO/test_strata_core_to_goto.sh
@@ -7,7 +7,7 @@
 # 3. Contract annotations on procedures
 # 4. Assertions in GOTO output
 
-set -eo pipefail
+set -euo pipefail
 
 SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)"
 PROJECT_ROOT="$(cd "$SCRIPT_DIR/../../../.." && pwd)"
@@ -34,13 +34,14 @@ assert 'checker' in st, 'checker not in symtab'
 print('  OK: helper and checker in symbol table')
 "
 
-# Test 3: Global variable in symbol table
+# Test 3: Global variable in symbol table with correct attributes
 "$PYTHON" -c "
 import json
 with open('$WORK/test_multi_proc.symtab.json') as f:
     st = json.load(f)['symbolTable']
 assert 'g' in st, 'global variable g not in symtab'
-print('  OK: global variable g in symbol table')
+assert st['g'].get('isStaticLifetime') is True, 'global variable g does not have static lifetime'
+print('  OK: global variable g with static lifetime in symbol table')
 "
 
 # Test 4: Contract annotations present

From 322038b75e9afa2278dc4f598814da1a6eee8759 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 27 Mar 2026 23:19:04 +0000
Subject: [PATCH 3/3] Migrate StrataCoreToGoto to `strata coreToGoto`
 subcommand
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Follow the pattern of PR #691 (StrataVerify → strata verify) and migrate
the standalone StrataCoreToGoto executable into a coreToGoto subcommand
of the strata CLI.

- Delete StrataCoreToGoto.lean, move logic into StrataMain.lean
- Use the shared Command/ParsedFlags infrastructure and exit code scheme
- Add .core.st to deriveBaseName suffix list
- Remove StrataCoreToGoto from lakefile.toml and defaultTargets
- Update test script, mkGotoBin.sh, README, and steering doc

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 .kiro/steering/structure.md                   |   3 +-
 README.md                                     |   2 +-
 StrataCoreToGoto.lean                         | 216 ------------------
 StrataMain.lean                               | 161 ++++++++++++-
 .../CBMC/GOTO/test_strata_core_to_goto.sh     |   8 +-
 .../Backends/CBMC/SimpleAdd/mkGotoBin.sh      |   2 +-
 lakefile.toml                                 |   5 +-
 7 files changed, 167 insertions(+), 230 deletions(-)
 delete mode 100644 StrataCoreToGoto.lean

diff --git a/.kiro/steering/structure.md b/.kiro/steering/structure.md
index 4445fa325..9a90e562a 100644
--- a/.kiro/steering/structure.md
+++ b/.kiro/steering/structure.md
@@ -180,8 +180,7 @@ Program-to-program translations for simplification and verification. Each has op
 **Main module:** `Strata.lean`
 
 **Executables:**
-- `strata` - Main CLI (includes `verify`, `check`, `toIon`, `print`, etc.)
-- `StrataCoreToGoto` - Strata Core to GOTO translation
+- `strata` - Main CLI (includes `verify`, `coreToGoto`, `check`, `toIon`, `print`, etc.)
 - `StrataToCBMC` - CBMC backend
 
 **Commands:**
diff --git a/README.md b/README.md
index 42203dc30..9d602b99b 100644
--- a/README.md
+++ b/README.md
@@ -42,7 +42,7 @@ Unit tests are run with `#guard_msgs` commands. No output means the tests passed
 To build executable files only and omit proof checks that might take a long time, use
 
 ```bash
-lake build strata:exe strata StrataToCBMC StrataCoreToGoto
+lake build strata:exe strata StrataToCBMC
 ```
 
 ## Running Analyses on Existing Strata Programs
diff --git a/StrataCoreToGoto.lean b/StrataCoreToGoto.lean
deleted file mode 100644
index 02bae518a..000000000
--- a/StrataCoreToGoto.lean
+++ /dev/null
@@ -1,216 +0,0 @@
-/-
-  Copyright Strata Contributors
-
-  SPDX-License-Identifier: Apache-2.0 OR MIT
--/
-
-import Strata.Backends.CBMC.GOTO.CoreToGOTOPipeline
-import Strata.Backends.CBMC.GOTO.DefaultSymbols
-import Strata.Backends.CBMC.CollectSymbols
-import Strata.Languages.Core.Verifier
-import Strata.Transform.CallElim
-import Strata.Util.IO
-
-open Strata
-
-def usageMessage : Std.Format :=
-  f!"Usage: StrataCoreToGoto [OPTIONS] <file.core.st>{Std.Format.line}\
-  {Std.Format.line}\
-  Translates a Strata Core program to CProver GOTO JSON files.{Std.Format.line}\
-  {Std.Format.line}\
-  Options:{Std.Format.line}\
-  {Std.Format.line}  \
-  --output-dir <dir>    Directory for output files (default: current directory){Std.Format.line}  \
-  --program-name <name> Program name for GOTO output (default: derived from filename){Std.Format.line}  \
-  --no-call-elim        Skip call elimination (keep raw calls for external DFCC)"
-
-structure GotoOptions where
-  outputDir : String := "."
-  programName : Option String := none
-  callElim : Bool := true
-
-def parseOptions (args : List String) : Except Std.Format (GotoOptions × String) :=
-  go {} args
-  where
-    go : GotoOptions → List String → Except Std.Format (GotoOptions × String)
-    | opts, "--output-dir" :: dir :: rest => go {opts with outputDir := dir} rest
-    | opts, "--program-name" :: name :: rest => go {opts with programName := some name} rest
-    | opts, "--no-call-elim" :: rest => go {opts with callElim := false} rest
-    | opts, [file] => .ok (opts, file)
-    | _, [] => .error "StrataCoreToGoto requires a .core.st file as input"
-    | _, args => .error f!"Unknown options: {args}"
-
-def deriveBaseName (file : String) : String :=
-  let name := System.FilePath.fileName file |>.getD file
-  if name.endsWith ".core.st" then (name.dropEnd 8).toString
-  else if name.endsWith ".st" then (name.dropEnd 3).toString
-  else name
-
-/-- Sanitize a program name to prevent path traversal in output filenames. -/
-def sanitizeProgramName (name : String) : Option String :=
-  let s := name.replace "/" "" |>.replace "\\" "" |>.replace ".." ""
-  if s.isEmpty then none else some s
-
-def main (args : List String) : IO UInt32 := do
-  match parseOptions args with
-  | .ok (opts, file) =>
-    unless file.endsWith ".core.st" do
-      IO.println "Error: expected a .core.st file"
-      IO.println f!"{usageMessage}"
-      return 1
-    let baseName := deriveBaseName file
-    let programName ← match sanitizeProgramName (opts.programName.getD baseName) with
-      | some n => pure n
-      | none => IO.println "Error: invalid program name"; return 1
-    let dir := System.FilePath.mk opts.outputDir
-    IO.FS.createDirAll dir
-
-    let text ← Strata.Util.readInputSource file
-    let inputCtx := Lean.Parser.mkInputContext text (Strata.Util.displayName file)
-    let dctx := Elab.LoadedDialects.builtin
-    let dctx := dctx.addDialect! Core
-    let leanEnv ← Lean.mkEmptyEnvironment 0
-    match Strata.Elab.elabProgram dctx leanEnv inputCtx with
-    | .error errors =>
-      for e in errors do
-        let msg ← e.toString
-        IO.println s!"Error: {msg}"
-      return 1
-    | .ok pgm =>
-      -- Type check (translates DDM Program → Core.Program)
-      let Env := Lambda.TEnv.default
-      let tcPgm ← match Strata.typeCheck inputCtx pgm with
-        | .ok p => pure p
-        | .error e => IO.println s!"Type check error: {e.message}"; return 1
-      IO.println "[Strata.Core] Type Checking Succeeded!"
-
-      -- Apply call elimination to inline contracts (assert requires / assume ensures)
-      let tcPgm ← if opts.callElim then
-        match Core.Transform.run tcPgm (fun p => do
-              let (_, p) ← Core.CallElim.callElim' p; return p) with
-        | .ok p => pure p
-        | .error e => IO.println s!"Call elimination error: {e}"; return 1
-      else pure tcPgm
-
-      -- Re-type-check after call elimination (discovers new variables)
-      let tcPgm ← match Core.typeCheck .default tcPgm with
-        | .ok p => pure p
-        | .error e => IO.println s!"Re-type-check error: {e}"; return 1
-
-      -- Apply GOTO pipeline passes
-      let tcPgm := inlineFuncDefsInProgram tcPgm
-      let tcPgm := inlineRecFuncDefsInProgram tcPgm
-      let tcPgm := partialEvalDatatypesInProgram tcPgm
-
-      -- Collect procedures and functions
-      let procs := tcPgm.decls.filterMap fun d => d.getProc?
-      let funcs := tcPgm.decls.filterMap fun d =>
-        match d.getFunc? with
-        | some f =>
-          let name := Core.CoreIdent.toPretty f.name
-          if f.body.isSome && f.typeArgs.isEmpty
-            && name != "Int.DivT" && name != "Int.ModT"
-          then some f else none
-        | none => none
-
-      if procs.isEmpty && funcs.isEmpty then
-        IO.println "Error: No procedures or functions found"
-        return 1
-
-      -- Collect axioms and type symbols
-      let axioms := tcPgm.decls.filterMap fun d => d.getAxiom?
-      let dtAxioms := generateDatatypeAxioms tcPgm
-      let recAxioms := generateRecFuncAxioms tcPgm (unrollDepth := 0)
-      let axioms := axioms ++ dtAxioms ++ recAxioms
-      let distincts := tcPgm.decls.filterMap fun d => match d with
-        | .distinct name es _ => some (name, es) | _ => none
-      let typeSyms ← match collectExtraSymbols tcPgm with
-        | .ok s => pure s
-        | .error e => IO.println s!"Error collecting symbols: {e}"; return 1
-      let gotoDtInfo := collectGotoDatatypeInfo tcPgm
-
-      -- Translate each procedure and function to GOTO
-      let mut symtabPairs : Array (String × Lean.Json) := #[]
-      let mut gotoFns : Array Lean.Json := #[]
-      let mut errors : Nat := 0
-      -- Seed type environment with global variable types
-      let globalVarEntries : Map Core.Expression.Ident Core.Expression.Ty :=
-        tcPgm.decls.filterMap fun d =>
-          match d with
-          | .var name ty _ _ => some (name, ty)
-          | _ => none
-      let Env := Lambda.TEnv.addInNewestContext
-        (T := ⟨Core.ExpressionMetadata, Unit⟩) Env globalVarEntries
-
-      let mut allLiftedFuncs : List Core.Function := []
-
-      for p in procs do
-        let procName := Core.CoreIdent.toPretty p.header.name
-        match procedureToGotoCtx Env p (axioms := axioms) (distincts := distincts)
-              (varTypes := tcPgm.getVarTy?) with
-        | .error e => IO.println s!"Error: skipping procedure {procName}: {e}"; errors := errors + 1
-        | .ok (ctx, liftedFuncs) =>
-          allLiftedFuncs := allLiftedFuncs ++ liftedFuncs
-          let ctx := rewriteDatatypeExprsInCtx gotoDtInfo ctx
-          let ctx ← lowerAddressOfInCtx ctx
-          let json ← IO.ofExcept (CoreToGOTO.CProverGOTO.Context.toJson procName ctx)
-          match json.symtab with
-          | .obj m => symtabPairs := symtabPairs ++ m.toList.toArray
-          | _ => pure ()
-          match json.goto with
-          | .obj m =>
-            match m.toList.find? (·.1 == "functions") with
-            | some (_, .arr fns) => gotoFns := gotoFns ++ fns
-            | _ => pure ()
-          | _ => pure ()
-
-      for f in funcs ++ allLiftedFuncs do
-        let funcName := Core.CoreIdent.toPretty f.name
-        match functionToGotoCtx Env f with
-        | .error e => IO.println s!"Error: skipping function {funcName}: {e}"; errors := errors + 1
-        | .ok ctx =>
-          let json ← IO.ofExcept (CoreToGOTO.CProverGOTO.Context.toJson funcName ctx)
-          match json.symtab with
-          | .obj m => symtabPairs := symtabPairs ++ m.toList.toArray
-          | _ => pure ()
-          match json.goto with
-          | .obj m =>
-            match m.toList.find? (·.1 == "functions") with
-            | some (_, .arr fns) => gotoFns := gotoFns ++ fns
-            | _ => pure ()
-          | _ => pure ()
-
-      if errors > 0 then
-        IO.println s!"Error: {errors} procedure/function translation(s) failed"
-        return 1
-
-      -- Add type symbols
-      match Lean.toJson typeSyms with
-      | .obj m => symtabPairs := symtabPairs ++ m.toList.toArray
-      | _ => pure ()
-
-      -- Deduplicate symbol table (later entries override earlier ones so that
-      -- collectExtraSymbols globals/datatypes take precedence)
-      let mut symtabMap : Std.HashMap String Lean.Json := {}
-      for (k, v) in symtabPairs do
-        symtabMap := symtabMap.insert k v
-
-      -- Add CBMC default symbols only if not already present
-      for (k, v) in CProverGOTO.defaultSymbols (moduleName := programName) do
-        if !symtabMap.contains k then
-          symtabMap := symtabMap.insert k (Lean.toJson v)
-
-      let symtab := Lean.Json.mkObj [("symbolTable", Lean.Json.mkObj symtabMap.toList)]
-      let goto := Lean.Json.mkObj [("functions", Lean.Json.arr gotoFns)]
-
-      let symTabFile := dir / s!"{programName}.symtab.json"
-      let gotoFile := dir / s!"{programName}.goto.json"
-      IO.FS.writeFile symTabFile symtab.pretty
-      IO.FS.writeFile gotoFile goto.pretty
-      IO.println s!"Translated {procs.length} procedures and {funcs.length} functions"
-      IO.println s!"Written {symTabFile} and {gotoFile}"
-      return 0
-  | .error msg =>
-    IO.println f!"{msg}"
-    IO.println f!"{usageMessage}"
-    return 1
diff --git a/StrataMain.lean b/StrataMain.lean
index c3be67030..8526f7a17 100644
--- a/StrataMain.lean
+++ b/StrataMain.lean
@@ -26,7 +26,9 @@ import Strata.Languages.Python.PythonRuntimeLaurelPart
 import Strata.Languages.Python.PythonLaurelCorePrelude
 import Strata.Backends.CBMC.CollectSymbols
 import Strata.Backends.CBMC.GOTO.CoreToGOTOPipeline
+import Strata.Backends.CBMC.GOTO.DefaultSymbols
 
+import Strata.Transform.CallElim
 import Strata.SimpleAPI
 
 open Strata
@@ -486,7 +488,7 @@ private def printPyAnalyzeSummary (vcResults : Array Core.VCResult)
 
 private def deriveBaseName (file : String) : String :=
   let name := System.FilePath.fileName file |>.getD file
-  let suffixes := [".python.st.ion", ".py.ion", ".st.ion", ".st"]
+  let suffixes := [".python.st.ion", ".py.ion", ".core.st", ".st.ion", ".st"]
   match suffixes.find? (name.endsWith ·) with
   | some sfx => (name.dropEnd sfx.length).toString
   | none     => name
@@ -1265,9 +1267,164 @@ def verifyCommand : Command where
       println! f!"Finished with {errors.size} errors."
       IO.Process.exit 1
 
+/-- Sanitize a program name to prevent path traversal in output filenames. -/
+private def sanitizeProgramName (name : String) : Option String :=
+  let s := name.replace "/" "" |>.replace "\\" "" |>.replace ".." ""
+  if s.isEmpty then none else some s
+
+def coreToGotoCommand : Command where
+  name := "coreToGoto"
+  args := [ "file" ]
+  flags := [
+    { name := "output-dir", help := "Directory for output files (default: current directory).",
+      takesArg := .arg "dir" },
+    { name := "program-name", help := "Program name for GOTO output (default: derived from filename).",
+      takesArg := .arg "name" },
+    { name := "no-call-elim", help := "Skip call elimination (keep raw calls for external DFCC)." } ]
+  help := "Translate a Strata Core program (.core.st) to CProver GOTO JSON files."
+  callback := fun v pflags => do
+    let file := v[0]
+    unless file.endsWith ".core.st" do
+      exitCmdFailure "coreToGoto" "expected a .core.st file"
+    let baseName := deriveBaseName file
+    let programName ← match sanitizeProgramName (pflags.getString "program-name" |>.getD baseName) with
+      | some n => pure n
+      | none => exitCmdFailure "coreToGoto" "invalid program name"
+    let dir := System.FilePath.mk (pflags.getString "output-dir" |>.getD ".")
+    IO.FS.createDirAll dir
+    let callElim := !pflags.getBool "no-call-elim"
+
+    let text ← Strata.Util.readInputSource file
+    let inputCtx := Lean.Parser.mkInputContext text (Strata.Util.displayName file)
+    let dctx := Elab.LoadedDialects.builtin |>.addDialect! Core
+    let leanEnv ← Lean.mkEmptyEnvironment 0
+    match Strata.Elab.elabProgram dctx leanEnv inputCtx with
+    | .error errors =>
+      for e in errors do IO.println s!"Error: {← e.toString}"
+      exitUserError "parsing failed"
+    | .ok pgm =>
+      let Env := Lambda.TEnv.default
+      let tcPgm ← match Strata.typeCheck inputCtx pgm with
+        | .ok p => pure p
+        | .error e => exitUserError s!"Type check error: {e.message}"
+      IO.println "[Strata.Core] Type Checking Succeeded!"
+
+      let tcPgm ← if callElim then
+        match Core.Transform.run tcPgm (fun p => do
+              let (_, p) ← Core.CallElim.callElim' p; return p) with
+        | .ok p => pure p
+        | .error e => exitInternalError s!"Call elimination error: {e}"
+      else pure tcPgm
+
+      let tcPgm ← match Core.typeCheck .default tcPgm with
+        | .ok p => pure p
+        | .error e => exitInternalError s!"Re-type-check error: {e}"
+
+      let tcPgm := inlineFuncDefsInProgram tcPgm
+      let tcPgm := inlineRecFuncDefsInProgram tcPgm
+      let tcPgm := partialEvalDatatypesInProgram tcPgm
+
+      let procs := tcPgm.decls.filterMap fun d => d.getProc?
+      let funcs := tcPgm.decls.filterMap fun d =>
+        match d.getFunc? with
+        | some f =>
+          let name := Core.CoreIdent.toPretty f.name
+          if f.body.isSome && f.typeArgs.isEmpty
+            && name != "Int.DivT" && name != "Int.ModT"
+          then some f else none
+        | none => none
+
+      if procs.isEmpty && funcs.isEmpty then
+        exitUserError "No procedures or functions found"
+
+      let axioms := tcPgm.decls.filterMap fun d => d.getAxiom?
+      let dtAxioms := generateDatatypeAxioms tcPgm
+      let recAxioms := generateRecFuncAxioms tcPgm (unrollDepth := 0)
+      let axioms := axioms ++ dtAxioms ++ recAxioms
+      let distincts := tcPgm.decls.filterMap fun d => match d with
+        | .distinct name es _ => some (name, es) | _ => none
+      let typeSyms ← match collectExtraSymbols tcPgm with
+        | .ok s => pure s
+        | .error e => exitInternalError s!"Error collecting symbols: {e}"
+      let gotoDtInfo := collectGotoDatatypeInfo tcPgm
+
+      let mut symtabPairs : Array (String × Lean.Json) := #[]
+      let mut gotoFns : Array Lean.Json := #[]
+      let mut errors : Nat := 0
+      let globalVarEntries : Map Core.Expression.Ident Core.Expression.Ty :=
+        tcPgm.decls.filterMap fun d =>
+          match d with
+          | .var name ty _ _ => some (name, ty)
+          | _ => none
+      let Env := Lambda.TEnv.addInNewestContext
+        (T := ⟨Core.ExpressionMetadata, Unit⟩) Env globalVarEntries
+
+      let mut allLiftedFuncs : List Core.Function := []
+
+      for p in procs do
+        let procName := Core.CoreIdent.toPretty p.header.name
+        match procedureToGotoCtx Env p (axioms := axioms) (distincts := distincts)
+              (varTypes := tcPgm.getVarTy?) with
+        | .error e => IO.println s!"Error: skipping procedure {procName}: {e}"; errors := errors + 1
+        | .ok (ctx, liftedFuncs) =>
+          allLiftedFuncs := allLiftedFuncs ++ liftedFuncs
+          let ctx := rewriteDatatypeExprsInCtx gotoDtInfo ctx
+          let ctx ← lowerAddressOfInCtx ctx
+          let json ← IO.ofExcept (CoreToGOTO.CProverGOTO.Context.toJson procName ctx)
+          match json.symtab with
+          | .obj m => symtabPairs := symtabPairs ++ m.toList.toArray
+          | _ => pure ()
+          match json.goto with
+          | .obj m =>
+            match m.toList.find? (·.1 == "functions") with
+            | some (_, .arr fns) => gotoFns := gotoFns ++ fns
+            | _ => pure ()
+          | _ => pure ()
+
+      for f in funcs ++ allLiftedFuncs do
+        let funcName := Core.CoreIdent.toPretty f.name
+        match functionToGotoCtx Env f with
+        | .error e => IO.println s!"Error: skipping function {funcName}: {e}"; errors := errors + 1
+        | .ok ctx =>
+          let json ← IO.ofExcept (CoreToGOTO.CProverGOTO.Context.toJson funcName ctx)
+          match json.symtab with
+          | .obj m => symtabPairs := symtabPairs ++ m.toList.toArray
+          | _ => pure ()
+          match json.goto with
+          | .obj m =>
+            match m.toList.find? (·.1 == "functions") with
+            | some (_, .arr fns) => gotoFns := gotoFns ++ fns
+            | _ => pure ()
+          | _ => pure ()
+
+      if errors > 0 then
+        exitInternalError s!"{errors} procedure/function translation(s) failed"
+
+      match Lean.toJson typeSyms with
+      | .obj m => symtabPairs := symtabPairs ++ m.toList.toArray
+      | _ => pure ()
+
+      let mut symtabMap : Std.HashMap String Lean.Json := {}
+      for (k, v) in symtabPairs do
+        symtabMap := symtabMap.insert k v
+
+      for (k, v) in CProverGOTO.defaultSymbols (moduleName := programName) do
+        if !symtabMap.contains k then
+          symtabMap := symtabMap.insert k (Lean.toJson v)
+
+      let symtab := Lean.Json.mkObj [("symbolTable", Lean.Json.mkObj symtabMap.toList)]
+      let goto := Lean.Json.mkObj [("functions", Lean.Json.arr gotoFns)]
+
+      let symTabFile := dir / s!"{programName}.symtab.json"
+      let gotoFile := dir / s!"{programName}.goto.json"
+      IO.FS.writeFile symTabFile symtab.pretty
+      IO.FS.writeFile gotoFile goto.pretty
+      IO.println s!"Translated {procs.length} procedures and {funcs.length} functions"
+      IO.println s!"Written {symTabFile} and {gotoFile}"
+
 def commandGroups : List CommandGroup := [
   { name := "Core"
-    commands := [verifyCommand, checkCommand, toIonCommand, printCommand, diffCommand]
+    commands := [verifyCommand, coreToGotoCommand, checkCommand, toIonCommand, printCommand, diffCommand]
     commonFlags := [includeFlag] },
   { name := "Code Generation"
     commands := [javaGenCommand] },
diff --git a/StrataTest/Backends/CBMC/GOTO/test_strata_core_to_goto.sh b/StrataTest/Backends/CBMC/GOTO/test_strata_core_to_goto.sh
index bd15209c8..cc066a78f 100755
--- a/StrataTest/Backends/CBMC/GOTO/test_strata_core_to_goto.sh
+++ b/StrataTest/Backends/CBMC/GOTO/test_strata_core_to_goto.sh
@@ -1,5 +1,5 @@
 #!/bin/bash
-# Test: StrataCoreToGoto translates multi-procedure programs with contracts.
+# Test: strata coreToGoto translates multi-procedure programs with contracts.
 #
 # Exercises:
 # 1. Multi-procedure translation (two procedures)
@@ -11,7 +11,7 @@ set -euo pipefail
 
 SCRIPT_DIR="$(cd "$(dirname "$0")" && pwd)"
 PROJECT_ROOT="$(cd "$SCRIPT_DIR/../../../.." && pwd)"
-STRATA_CORE_TO_GOTO="$PROJECT_ROOT/.lake/build/bin/StrataCoreToGoto"
+STRATA="$PROJECT_ROOT/.lake/build/bin/strata"
 PYTHON=${PYTHON:-python3}
 
 WORK=$(mktemp -d)
@@ -21,7 +21,7 @@ INPUT="$SCRIPT_DIR/test_multi_proc.core.st"
 
 # Test 1: Multi-procedure translation succeeds
 echo "Test 1: Multi-procedure translation"
-"$STRATA_CORE_TO_GOTO" --output-dir "$WORK" "$INPUT" 2>&1 | grep -q "Translated 2 procedures"
+"$STRATA" coreToGoto --output-dir "$WORK" "$INPUT" 2>&1 | grep -q "Translated 2 procedures"
 echo "  OK: translated 2 procedures"
 
 # Test 2: Both procedures in symbol table
@@ -73,4 +73,4 @@ for fn in data['functions']:
         break
 "
 
-echo "PASS: all StrataCoreToGoto tests passed"
+echo "PASS: all strata coreToGoto tests passed"
diff --git a/StrataTest/Backends/CBMC/SimpleAdd/mkGotoBin.sh b/StrataTest/Backends/CBMC/SimpleAdd/mkGotoBin.sh
index 3d642c219..cbaf0a508 100755
--- a/StrataTest/Backends/CBMC/SimpleAdd/mkGotoBin.sh
+++ b/StrataTest/Backends/CBMC/SimpleAdd/mkGotoBin.sh
@@ -6,7 +6,7 @@ rm -f *.gb
 
 echo "Writing out JSON files from a Strata Core program SimpleAdd"
 pushd ../../../../
-lake exe StrataCoreToGoto --output-dir StrataTest/Backends/CBMC/SimpleAdd StrataTest/Backends/CBMC/SimpleAdd/simpleAdd.core.st
+lake exe strata coreToGoto --output-dir StrataTest/Backends/CBMC/SimpleAdd StrataTest/Backends/CBMC/SimpleAdd/simpleAdd.core.st
 popd
 
 # The symtab.json now includes CBMC default symbols directly.
diff --git a/lakefile.toml b/lakefile.toml
index 60070b7d0..4c1625c98 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -1,6 +1,6 @@
 name = "Strata"
 version = "0.1.0"
-defaultTargets = ["Strata", "strata", "StrataMain", "StrataToCBMC", "StrataCoreToGoto"]
+defaultTargets = ["Strata", "strata", "StrataMain", "StrataToCBMC"]
 testDriver = "StrataTest"
 
 [[require]]
@@ -26,8 +26,5 @@ globs = ["StrataTest.+"]
 [[lean_exe]]
 name = "StrataToCBMC"
 
-[[lean_exe]]
-name = "StrataCoreToGoto"
-
 [[lean_exe]]
 name = "DiffTestCore"