@[reducible, inline]

abbrev CoreParams : Lambda.LExprParams

Equations

• CoreParams = { Metadata := Unit, IDMeta := Unit }

@[reducible, inline]

abbrev Core.ExprStr : Imperative.PureExpr

Equations

• One or more equations did not get rendered due to their size.

def CoreToGOTO.lookupType (T : Core.Expression.TyEnv) (i : Core.Expression.Ident) : Except Std.Format CProverGOTO.Ty

Equations

• One or more equations did not get rendered due to their size.

def CoreToGOTO.updateType (T : Core.Expression.TyEnv) (i : Core.Expression.Ident) (ty : Core.Expression.Ty) : Core.Expression.TyEnv

Equations

• CoreToGOTO.updateType T i ty = Lambda.TEnv.addInNewestContext T [(i, ty)]

@[implicit_reducible]

instance CoreToGOTO.instToGotoExpression : Imperative.ToGoto Core.Expression

Equations

• One or more equations did not get rendered due to their size.

def CoreToGOTO.lookupTypeStr (T : Core.ExprStr.TyEnv) (i : Core.ExprStr.Ident) : Except Std.Format CProverGOTO.Ty

Equations

• One or more equations did not get rendered due to their size.

def CoreToGOTO.updateTypeStr (T : Core.ExprStr.TyEnv) (i : Core.ExprStr.Ident) (ty : Core.ExprStr.Ty) : Core.ExprStr.TyEnv

Equations

• CoreToGOTO.updateTypeStr T i ty = Lambda.TEnv.addInNewestContext T [(i, ty)]

@[implicit_reducible]

instance CoreToGOTO.instToGotoExprStr : Imperative.ToGoto Core.ExprStr

Equations

• One or more equations did not get rendered due to their size.

def CoreToGOTO.substVarNames {Metadata IDMeta : Type} [DecidableEq IDMeta] (e : Lambda.LExpr { base := { Metadata := Metadata, IDMeta := IDMeta }, TypeType := Lambda.LMonoTy }) (frto : Map String String) : Lambda.LExpr { base := { Metadata := Unit, IDMeta := Unit }, TypeType := Lambda.LMonoTy }

Equations

• CoreToGOTO.substVarNames (Lambda.LExpr.const m c) frto = Lambda.LExpr.const () c
• CoreToGOTO.substVarNames (Lambda.LExpr.bvar m b) frto = Lambda.LExpr.bvar () b
• CoreToGOTO.substVarNames (Lambda.LExpr.op m o ty) frto = Lambda.LExpr.op () { name := o.name, metadata := () } ty
• CoreToGOTO.substVarNames (Lambda.LExpr.fvar m name ty) frto = Lambda.LExpr.fvar () { name := (frto.find? name.name).getD name.name, metadata := () } ty
• CoreToGOTO.substVarNames (Lambda.LExpr.abs m name ty e') frto = Lambda.LExpr.abs () name ty (CoreToGOTO.substVarNames e' frto)
• CoreToGOTO.substVarNames (Lambda.LExpr.quant m qk name ty tr' e') frto = Lambda.LExpr.quant () qk name ty (CoreToGOTO.substVarNames tr' frto) (CoreToGOTO.substVarNames e' frto)
• CoreToGOTO.substVarNames (Lambda.LExpr.app m f e') frto = Lambda.LExpr.app () (CoreToGOTO.substVarNames f frto) (CoreToGOTO.substVarNames e' frto)
• CoreToGOTO.substVarNames (Lambda.LExpr.ite m c t e') frto = Lambda.LExpr.ite () (CoreToGOTO.substVarNames c frto) (CoreToGOTO.substVarNames t frto) (CoreToGOTO.substVarNames e' frto)
• CoreToGOTO.substVarNames (Lambda.LExpr.eq m e1 e2) frto = Lambda.LExpr.eq () (CoreToGOTO.substVarNames e1 frto) (CoreToGOTO.substVarNames e2 frto)

def CoreToGOTO.convertMetaData (md : Imperative.MetaData Core.Expression) : Imperative.MetaData Core.ExprStr

Convert metadata from Core.Expression to Core.ExprStr, preserving label-keyed elements (fileRange, propertySummary, etc.) and dropping variable-keyed elements whose identifier type changes.

Equations

• One or more equations did not get rendered due to their size.

def CoreToGOTO.Core.Cmd.renameVars (frto : Map String String) (c : Imperative.Cmd Core.Expression) : Imperative.Cmd Core.ExprStr

Equations

• One or more equations did not get rendered due to their size.
• CoreToGOTO.Core.Cmd.renameVars frto (Imperative.Cmd.assume label e md) = Imperative.Cmd.assume label (CoreToGOTO.substVarNames e frto) (CoreToGOTO.convertMetaData md)
• CoreToGOTO.Core.Cmd.renameVars frto (Imperative.Cmd.assert label e md) = Imperative.Cmd.assert label (CoreToGOTO.substVarNames e frto) (CoreToGOTO.convertMetaData md)
• CoreToGOTO.Core.Cmd.renameVars frto (Imperative.Cmd.cover label e md) = Imperative.Cmd.cover label (CoreToGOTO.substVarNames e frto) (CoreToGOTO.convertMetaData md)

def CoreToGOTO.Core.Cmds.renameVars (frto : Map String String) (cs : Imperative.Cmds Core.Expression) : Imperative.Cmds Core.ExprStr

Equations

• CoreToGOTO.Core.Cmds.renameVars frto [] = []
• CoreToGOTO.Core.Cmds.renameVars frto (c :: crest) = [CoreToGOTO.Core.Cmd.renameVars frto c] ++ CoreToGOTO.Core.Cmds.renameVars frto crest

structure CoreToGOTO.CProverGOTO.Context : Type

• program : CProverGOTO.Program
• locals : List String
• formals : Map String CProverGOTO.Ty
• ret : CProverGOTO.Ty
• contracts : List (String × Lean.Json)

  Contract annotations for the code type (e.g., #spec_requires, #spec_ensures).

• localTypes : Std.HashMap String CProverGOTO.Ty

  Optional types for local variables (output parameters, typed locals).

structure CoreToGOTO.CProverGOTO.Json : Type

• symtab : Lean.Json
• goto : Lean.Json

def CoreToGOTO.CProverGOTO.Context.toJson (programName : String) (ctx : Context) : Except String Json

Equations

• One or more equations did not get rendered due to their size.

def CoreToGOTO.transformToGoto (cprog : Core.Program) : Except Std.Format CProverGOTO.Context

Equations

• One or more equations did not get rendered due to their size.

def CoreToGOTO.getGotoJson (programName : String) (env : Strata.Program) : IO CProverGOTO.Json

Equations

• One or more equations did not get rendered due to their size.

def CoreToGOTO.writeToGotoJson (programName symTabFileName gotoFileName : String) (env : Strata.Program) : IO Unit

Equations

• One or more equations did not get rendered due to their size.