Eliminate Python dependency from CBMC pipeline (#576)

The CBMC backend relied on a Python post-processing step
(process_json.py) to merge a 4000-line defaults.json of built-in symbols
into the Lean-generated symbol table before passing it to symtab2gb.
This made the pipeline harder to maintain, required Python as a runtime
dependency, and kept critical symbol definitions outside of Lean where
they could not benefit from type checking.

*Description of changes:*

Generate all 38 CBMC built-in symbols directly in Lean
(DefaultSymbols.lean), parameterized by ArchConfig and module name, and
emit the symbol table in the {"symbolTable": ...} wrapper that symtab2gb
expects. This turns the pipeline into a simple two-step flow (strata →
symtab2gb) with no Python intermediary.

Remove the now-unused Python scripts (process_json.py, defaults.py),
defaults.json, and legacy shell wrappers (run_strata_cbmc.sh,
compare_cbmc_json.sh). Update all pipeline scripts and documentation to
reflect the simplified flow.

By submitting this pull request, I confirm that you can use, modify,
copy, and redistribute this contribution, under the terms of your
choice.

---------

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
Co-authored-by: Shilpi Goel <shigoel@gmail.com>

Author: 3 people

.github/workflows/cbmc.yml

@@ -95,8 +95,12 @@ jobs:
       - name: Run legacy CBMC test (C_Simp)
         shell: bash
         run: |
-          export CBMC_DIR="$(dirname $(which cbmc))/"
-          ./Strata/Backends/CBMC/run_strata_cbmc.sh Strata/Backends/CBMC/tests/simpleTest.csimp.st
+          lake exe StrataToCBMC Strata/Backends/CBMC/tests/simpleTest.csimp.st > symtab.json
+          symtab2gb symtab.json --out full.goto
+          goto-instrument --enforce-contract simpleTest full.goto full_checking.goto
+          OUTPUT=$(cbmc full_checking.goto --function simpleTest --trace)
+          echo "$OUTPUT"
+          [[ "$OUTPUT" == *"VERIFICATION SUCCESSFUL"* ]]
       - name: Run Python CBMC pipeline tests
         shell: bash
         run: |

Strata/Backends/CBMC/GOTO/CoreToCProverGOTO.lean

@@ -6,6 +6,7 @@
 
 import Strata.Languages.Core.Verifier
 import Strata.Backends.CBMC.GOTO.InstToJson
+import Strata.Backends.CBMC.GOTO.DefaultSymbols
 import Strata.Backends.CBMC.GOTO.LambdaToCProverGOTO
 import Strata.DL.Imperative.ToCProverGOTO
 
@@ -261,7 +262,9 @@ def getGotoJson (programName : String) (env : Program) : IO CProverGOTO.Json :=
 open Strata in
 def writeToGotoJson (programName symTabFileName gotoFileName : String) (env : Program) : IO Unit := do
   let json ← getGotoJson programName env
-  IO.FS.writeFile symTabFileName json.symtab.pretty
+  let symtabObj := match json.symtab with | .obj m => m | _ => .empty
+  let symtab := CProverGOTO.wrapSymtab symtabObj (moduleName := programName)
+  IO.FS.writeFile symTabFileName symtab.pretty
   IO.FS.writeFile gotoFileName json.goto.pretty
 
 end CoreToGOTO

Strata/Backends/CBMC/GOTO/CoreToGOTOPipeline.lean

@@ -400,7 +400,7 @@ symtab/goto JSON.
 -/
 def emitProcWithLifted (Env : Core.Expression.TyEnv) (procName : String)
     (ctx : CoreToGOTO.CProverGOTO.Context) (liftedFuncs : List Core.Function)
-    (extraSyms : Lean.Json)
+    (extraSyms : Lean.Json) (moduleName : String)
     : IO (Lean.Json × Lean.Json) := do
   let json ← IO.ofExcept (CoreToGOTO.CProverGOTO.Context.toJson procName ctx)
   let mut symtabObj := match json.symtab with | .obj m => m | _ => .empty
@@ -427,7 +427,8 @@ def emitProcWithLifted (Env : Core.Expression.TyEnv) (procName : String)
   | .obj m => for (k, v) in m.toList do
       symtabObj := symtabObj.insert k v
   | _ => pure ()
-  return (Lean.Json.obj symtabObj, Lean.Json.mkObj [("functions", Lean.Json.arr gotoFns)])
+  let symtab := CProverGOTO.wrapSymtab symtabObj (moduleName := moduleName)
+  return (symtab, Lean.Json.mkObj [("functions", Lean.Json.arr gotoFns)])
 
 /-! ## High-level pipeline steps
 
@@ -493,7 +494,7 @@ public def coreToGotoFiles (tcPgm : Core.Program) (Env : Core.Expression.TyEnv)
       | .ok s => pure (Lean.toJson s)
       | .error e => throw s!"{e}"
     let (symtab, goto) ←
-      match ← emitProcWithLifted Env procName ctx liftedFuncs extraSyms |>.toBaseIO with
+      match ← emitProcWithLifted Env procName ctx liftedFuncs extraSyms (moduleName := baseName) |>.toBaseIO with
       | .ok r => pure r
       | .error e => throw s!"{e}"
     let symTabFile := s!"{baseName}.symtab.json"