Remove custom SizeOf instances.

Strata/Backends/CBMC/CoreToCBMC.lean

@@ -181,8 +181,6 @@ def blockToJson {P : Imperative.PureExpr} (I : Lambda.LExprParams) [IdentToStr (
     ]),
     ("sub", Json.arr (b.map (stmtToJson (I:=I) · loc)).toArray)
   ]
-  termination_by (Imperative.Block.sizeOf b)
-  decreasing_by term_by_mem [Stmt, Imperative.sizeOf_stmt_in_block]
 
 def stmtToJson {P : Imperative.PureExpr} (I : Lambda.LExprParams) [IdentToStr (Lambda.Identifier I.IDMeta)] [HasLExpr P I]
   (e : Imperative.Stmt P Command) (loc: SourceLoc) : Json :=
@@ -204,8 +202,6 @@ def stmtToJson {P : Imperative.PureExpr} (I : Lambda.LExprParams) [IdentToStr (L
       ])
     ]
   | _ => panic! "Unimplemented"
-  termination_by (Imperative.Stmt.sizeOf e)
-  decreasing_by all_goals term_by_mem
 end
 
 def listToExpr (l: ListMap CoreLabel Core.Procedure.Check) : Core.Expression.Expr :=

Strata/Backends/CBMC/StrataToCBMC.lean

@@ -302,8 +302,6 @@ def blockToJson (b: Imperative.Block Strata.C_Simp.Expression Strata.C_Simp.Comm
     ]),
     ("sub", Json.arr (b.map (stmtToJson · loc)).toArray)
   ]
-  termination_by b.sizeOf
-  decreasing_by term_by_mem [Stmt, Imperative.sizeOf_stmt_in_block]
 
  def stmtToJson (e : Strata.C_Simp.Statement) (loc: SourceLoc) : Json :=
   match e with
@@ -323,7 +321,6 @@ def blockToJson (b: Imperative.Block Strata.C_Simp.Expression Strata.C_Simp.Comm
       ])
     ]
   | _ => panic! "Unimplemented"
-  termination_by e.sizeOf
 end
 
 def createImplementationSymbolFromAST (func : Strata.C_Simp.Function) : CBMCSymbol :=

Strata/DL/Imperative/Cmd.lean

@@ -67,22 +67,6 @@ def Cmd.getMetaData (c : Cmd P) : MetaData P :=
   | .assert _ _ md | .assume _ _ md | .cover _ _ md =>
    md
 
-instance : SizeOf String where
-  sizeOf s := s.length
-
-@[simp]
-def Cmd.sizeOf (c : Imperative.Cmd P) : Nat :=
-  match c with
-  | .init   n t eOpt _ => 1 + SizeOf.sizeOf n + SizeOf.sizeOf t + (match eOpt with | some e => SizeOf.sizeOf e | none => 0)
-  | .set    n e _ => 1 + SizeOf.sizeOf n + SizeOf.sizeOf e
-  | .havoc  n _ => 1 + SizeOf.sizeOf n
-  | .assert l b _ => 1 + SizeOf.sizeOf l + SizeOf.sizeOf b
-  | .assume l b _ => 1 + SizeOf.sizeOf l + SizeOf.sizeOf b
-  | .cover l b _ => 1 + SizeOf.sizeOf l + SizeOf.sizeOf b
-
-instance (P : PureExpr) : SizeOf (Imperative.Cmd P) where
-  sizeOf := Cmd.sizeOf
-
 ---------------------------------------------------------------------
 
 class HasPassiveCmds (P : PureExpr) (CmdT : Type) where

Strata/DL/Imperative/Stmt.lean

@@ -94,7 +94,7 @@ def Stmt.inductionOn {P : PureExpr} {Cmd : Type}
 
 ---------------------------------------------------------------------
 
-/-! ### SizeOf -/
+/-! ### sizeOf -/
 
 mutual
 @[simp]
@@ -115,18 +115,6 @@ def Block.sizeOf (ss : Imperative.Block P C) : Nat :=
 
 end
 
-theorem sizeOf_stmt_in_block {s : Imperative.Stmt P C} {b: Imperative.Block P C} (s_in: s ∈ b) : s.sizeOf < b.sizeOf := by
-  induction b with
-  | nil => grind
-  | cons hd tl IH =>
-    rw[List.mem_cons] at s_in; simp only [Block.sizeOf]; grind
-
-instance (P : PureExpr) : SizeOf (Imperative.Stmt P C) where
-  sizeOf := Stmt.sizeOf
-
-instance (P : PureExpr) : SizeOf (Imperative.Block P C) where
-  sizeOf := Block.sizeOf
-
 ---------------------------------------------------------------------
 
 /--
@@ -143,7 +131,6 @@ def Stmt.hasLabelInside (label : String) (s : Stmt P C) : Bool :=
   |  .block label' bss _ => label = label' || Block.hasLabelInside label bss
   |  .ite _ tss ess _ => Block.hasLabelInside label tss || Block.hasLabelInside label ess
   |  _ => false
-  termination_by (Stmt.sizeOf s)
 
 /--
 Do statements `ss` contain any block labeled `label`?
@@ -152,7 +139,6 @@ def Block.hasLabelInside (label : String) (ss : List (Stmt P C)) : Bool :=
   match ss with
   | [] => false
   | s :: ss => Stmt.hasLabelInside label s || Block.hasLabelInside label ss
-  termination_by (Block.sizeOf ss)
 end
 
 ---------------------------------------------------------------------
@@ -232,13 +218,11 @@ def Stmt.getVars [HasVarsPure P P.Expr] [HasVarsPure P C] (s : Stmt P C) : List
       let bodyVars := HasVarsPure.getVars body
       let formals := decl.inputs.map (·.1)
       bodyVars.filter (fun v => formals.all (fun f => ¬(P.EqIdent v f).decide))
-  termination_by (Stmt.sizeOf s)
 
 def Block.getVars [HasVarsPure P P.Expr] [HasVarsPure P C] (ss : Block P C) : List P.Ident :=
   match ss with
   | [] => []
   | s :: srest => Stmt.getVars s ++ Block.getVars srest
-  termination_by (Block.sizeOf ss)
 end
 
 instance (P : PureExpr) [HasVarsPure P P.Expr] [HasVarsPure P C]
@@ -259,13 +243,11 @@ def Stmt.definedVars [HasVarsImp P C] (s : Stmt P C) : List P.Ident :=
   | .loop _ _ _ body _ => Block.definedVars body
   | .funcDecl decl _ => [decl.name]  -- Function declaration defines the function name
   | _ => []
-  termination_by (Stmt.sizeOf s)
 
 def Block.definedVars [HasVarsImp P C] (ss : Block P C) : List P.Ident :=
   match ss with
   | [] => []
   | s :: srest => Stmt.definedVars s ++ Block.definedVars srest
-  termination_by (Block.sizeOf ss)
 end
 
 mutual
@@ -278,13 +260,11 @@ def Stmt.modifiedVars [HasVarsImp P C] (s : Stmt P C) : List P.Ident :=
   | .ite _ tbss ebss _ => Block.modifiedVars tbss ++ Block.modifiedVars ebss
   | .loop _ _ _ bss _ => Block.modifiedVars bss
   | .funcDecl _ _ => []  -- Function declarations don't modify variables
-  termination_by (Stmt.sizeOf s)
 
 def Block.modifiedVars [HasVarsImp P C] (ss : Block P C) : List P.Ident :=
   match ss with
   | [] => []
   | s :: srest => Stmt.modifiedVars s ++ Block.modifiedVars srest
-  termination_by (Block.sizeOf ss)
 end
 
 mutual
@@ -297,14 +277,12 @@ def Stmt.touchedVars [HasVarsImp P C] (s : Stmt P C) : List P.Ident :=
   | .block _ bss _ => Block.touchedVars bss
   | .ite _ tbss ebss _ => Block.touchedVars tbss ++ Block.touchedVars ebss
   | _ => Stmt.definedVars s ++ Stmt.modifiedVars s
-  termination_by (Stmt.sizeOf s)
 
 @[simp]
 def Block.touchedVars [HasVarsImp P C] (ss : Block P C) : List P.Ident :=
   match ss with
   | [] => []
   | s :: srest => Stmt.touchedVars s ++ Block.touchedVars srest
-  termination_by (Block.sizeOf ss)
 end
 
 instance (P : PureExpr) [HasVarsImp P C] : HasVarsImp P (Stmt P C) where
@@ -343,7 +321,6 @@ def formatStmt (P : PureExpr) (s : Stmt P C)
       f!"{md}while{children}"
   | .goto label md => f!"{md}goto {label}"
   | .funcDecl _ md => f!"{md}funcDecl <function>"
-  termination_by s.sizeOf
 
 def formatBlock (P : PureExpr) (ss : List (Stmt P C))
   [ToFormat P.Ident] [ToFormat P.Expr] [ToFormat P.Ty] [ToFormat C] : Format :=
@@ -352,8 +329,6 @@ def formatBlock (P : PureExpr) (ss : List (Stmt P C))
     | parts =>
       let inner := line ++ (group $ joinSep (parts.map (fun s => formatStmt P s)) (format "\n"))
       f!"\{{nestD inner}\n}"
-  termination_by (Block.sizeOf ss)
-  decreasing_by all_goals (simp_wf; apply sizeOf_stmt_in_block; simp_all)
 end
 
 

Strata/DL/Imperative/StmtSemantics.lean

@@ -152,8 +152,6 @@ theorem EvalStmtDefMonotone
   | .goto _ _ => cases Heval
   | .loop _ _ _ _ _ => cases Heval
   | .funcDecl _ _ => cases Heval; assumption
-  termination_by (Stmt.sizeOf s)
-  decreasing_by all_goals term_by_mem
 
 theorem EvalBlockDefMonotone
   [DecidableEq P.Ident]
@@ -174,6 +172,4 @@ theorem EvalBlockDefMonotone
     apply EvalBlockDefMonotone (σ:=σ1) (δ:=δ1)
     apply EvalStmtDefMonotone <;> assumption
     assumption
-  termination_by (Block.sizeOf ss)
-  decreasing_by all_goals term_by_mem
 end

Strata/DL/Lambda/LExpr.lean

@@ -259,9 +259,6 @@ def LExpr.sizeOf: LExpr T → Nat
   | LExpr.eq _ e1 e2 => 3 + sizeOf e1 + sizeOf e2
   | _ => 1
 
-instance  : SizeOf (LExpr T) where
-  sizeOf := LExpr.sizeOf
-
 /--
 Get type of a constant `c`
 -/

Strata/Languages/C_Simp/C_Simp.lean

@@ -36,9 +36,9 @@ abbrev Expression : Imperative.PureExpr := {
 }
 
 
-def Command := Imperative.Cmd Expression
+abbrev Command := Imperative.Cmd Expression
 
-def Statement := Imperative.Stmt Expression Command
+abbrev Statement := Imperative.Stmt Expression Command
 
 instance : Imperative.HasVarsImp Expression Command where
   definedVars := Imperative.Cmd.definedVars

Strata/Languages/C_Simp/Verify.lean

@@ -50,9 +50,6 @@ def translate_stmt (s: Imperative.Stmt C_Simp.Expression C_Simp.Command) : Core.
   | .loop guard measure invariant body _md => .loop (translate_expr guard) (translate_opt_expr measure) (translate_opt_expr invariant) (body.map translate_stmt) {}
   | .funcDecl _ _ => panic! "C_Simp does not support function declarations"
   | .goto label _md => .goto label {}
-  termination_by s.sizeOf
-  decreasing_by
-  all_goals term_by_mem [Imperative.Stmt, Imperative.sizeOf_stmt_in_block]
 
 
 /--

Strata/Languages/Core/OldExpressions.lean

@@ -126,8 +126,6 @@ def normalizeOldExpr (e : Expression.Expr) (inOld : Bool := false)
   | .ite m c t f => .ite m (normalizeOldExpr c inOld)
                       (normalizeOldExpr t inOld) (normalizeOldExpr f inOld)
   | .eq m e1 e2 => .eq m (normalizeOldExpr e1 inOld) (normalizeOldExpr e2 inOld)
-    termination_by sizeOf e
-  decreasing_by all_goals (simp[sizeOf, Lambda.LExpr.sizeOf]; try term_by_mem)
 
 def normalizeOldExprs (sm : List Expression.Expr) :=
   sm.map normalizeOldExpr

Strata/Languages/Core/Statement.lean

@@ -48,14 +48,6 @@ instance : HasPassiveCmds Expression Command where
 instance : HasHavoc Expression Command where
   havoc x := .cmd (.havoc x)
 
-def CmdExt.sizeOf (c : CmdExt P) : Nat :=
-  match c with
-  | .cmd c => SizeOf.sizeOf c
-  | .call l p a _ => 3 + l.length + SizeOf.sizeOf p + a.length
-
-instance : SizeOf (CmdExt P) where
-  sizeOf := CmdExt.sizeOf
-
 instance [ToFormat (Cmd P)] [ToFormat (MetaData P)]
     [ToFormat (List P.Ident)] [ToFormat P.Expr] :
     ToFormat (CmdExt P) where
@@ -135,15 +127,11 @@ def Statement.eraseTypes (s : Statement) : Statement :=
       axioms := decl.axioms.map Lambda.LExpr.eraseTypes,
       preconditions := decl.preconditions.map fun p => { p with expr := p.expr.eraseTypes } }
     .funcDecl decl' md
-  termination_by (Stmt.sizeOf s)
-  decreasing_by all_goals simp[sizeOf] <;> term_by_mem
 
 def Statements.eraseTypes (ss : Statements) : Statements :=
   match ss with
   | [] => []
   | s :: srest => Statement.eraseTypes s :: Statements.eraseTypes srest
-  termination_by (sizeOf ss)
-  decreasing_by all_goals simp [sizeOf] <;> term_by_mem
 end
 
 ---------------------------------------------------------------------
@@ -212,7 +200,6 @@ def Statement.modifiedVarsTrans
   | .loop _ _ _ bss _ =>
     Statements.modifiedVarsTrans π bss
   | .funcDecl _ _ => []  -- Function declarations don't modify variables
-  termination_by (Stmt.sizeOf s)
 
 def Statements.modifiedVarsTrans
   {ProcType : Type}
@@ -221,7 +208,6 @@ def Statements.modifiedVarsTrans
   : List Expression.Ident := match ss with
   | [] => []
   | s :: ss => Statement.modifiedVarsTrans π s ++ Statements.modifiedVarsTrans π ss
-  termination_by (Block.sizeOf ss)
 end
 
 def Command.getVarsTrans
@@ -258,7 +244,6 @@ def Statement.getVarsTrans
       let bodyVars := HasVarsPure.getVars body
       let formals := decl.inputs.map (·.1)
       bodyVars.filter (fun v => formals.all (fun f => v.name != f.name))
-  termination_by (Stmt.sizeOf s)
 
 def Statements.getVarsTrans
   {ProcType : Type}
@@ -267,7 +252,6 @@ def Statements.getVarsTrans
   : List Expression.Ident := match ss with
   | [] => []
   | s :: ss => Statement.getVarsTrans π s ++ Statements.getVarsTrans π ss
-  termination_by (Block.sizeOf ss)
 end
 
 -- don't need to transitively lookup for procedures
@@ -302,7 +286,6 @@ def Statement.touchedVarsTrans
   | .ite _ tbss ebss _ => Statements.touchedVarsTrans π tbss ++ Statements.touchedVarsTrans π ebss
   | .loop _ _ _ bss _ => Statements.touchedVarsTrans π bss
   | .funcDecl decl _ => [decl.name]  -- Function declaration touches (defines) the function name
-  termination_by (Stmt.sizeOf s)
 
 def Statements.touchedVarsTrans
   {ProcType : Type}
@@ -312,7 +295,6 @@ def Statements.touchedVarsTrans
   match ss with
   | [] => []
   | s :: srest => Statement.touchedVarsTrans π s ++ Statements.touchedVarsTrans π srest
-  termination_by (Block.sizeOf ss)
 end
 
 def Statement.allVarsTrans
@@ -332,8 +314,6 @@ mutual
 def Block.substFvar (b : Block) (fr:Expression.Ident)
       (to:Expression.Expr) : Block :=
   List.map (fun s => Statement.substFvar s fr to) b
-  termination_by b.sizeOf
-  decreasing_by term_by_mem [Stmt, sizeOf_stmt_in_block]
 
 def Statement.substFvar (s : Core.Statement)
       (fr:Expression.Ident)
@@ -371,7 +351,6 @@ def Statement.substFvar (s : Core.Statement)
       body := decl.body.map (Lambda.LExpr.substFvar · fr to),
       axioms := decl.axioms.map (Lambda.LExpr.substFvar · fr to) }
     .funcDecl decl' md
-  termination_by s.sizeOf
 end
 
 ---------------------------------------------------------------------
@@ -380,8 +359,6 @@ mutual
 def Block.renameLhs (b : Block)
     (fr: Lambda.Identifier Visibility) (to: Lambda.Identifier Visibility) : Block :=
   List.map (fun s => Statement.renameLhs s fr to) b
-  termination_by b.sizeOf
-  decreasing_by term_by_mem [Stmt, sizeOf_stmt_in_block]
 
 def Statement.renameLhs (s : Core.Statement)
     (fr: Lambda.Identifier Visibility) (to: Lambda.Identifier Visibility)
@@ -406,8 +383,6 @@ def Statement.renameLhs (s : Core.Statement)
     let decl' := if decl.name == fr then { decl with name := to } else decl
     .funcDecl decl' md
   | .assert _ _ _ | .assume _ _ _ | .cover _ _ _ | .goto _ _ => s
-  termination_by s.sizeOf
-  decreasing_by all_goals term_by_mem
 end
 
 ---------------------------------------------------------------------

Strata/Languages/Core/StatementType.lean

@@ -95,20 +95,19 @@ where
           .ok (Stmt.cmd c', Env, C)
 
         | .block label bss md => do
-          let Env := Env.pushEmptyContext
-          let (ss', Env, C) ← go C Env bss []
-          let s' := Stmt.block label ss' md
-          .ok (s', Env.popContext, C)
+          let (bss', Env, C) ← goBlock C Env bss []
+          let s' := Stmt.block label bss' md
+          .ok (s', Env, C)
 
         | .ite cond tss ess md => do try
           let _ ← Env.freeVarCheck cond f!"[{s}]" |>.mapError DiagnosticModel.fromFormat
           let (conda, Env) ← LExpr.resolve C Env cond |>.mapError DiagnosticModel.fromFormat
           let condty := conda.toLMonoTy
           match condty with
           | .tcons "bool" [] =>
-            let (tb, Env, C) ← go C Env [(Stmt.block "$_then" tss  #[])] []
-            let (eb, Env, C) ← go C Env [(Stmt.block "$_else" ess  #[])] []
-            let s' := Stmt.ite conda.unresolved tb eb md
+            let (tss, Env, C) ← goBlock C Env tss []
+            let (ess, Env, C) ← goBlock C Env ess []
+            let s' := Stmt.ite conda.unresolved tss ess md
             .ok (s', Env, C)
           | _ => .error <| md.toDiagnosticF f!"[{s}]: If's condition {cond} is not of type `bool`!"
           catch e =>
@@ -138,7 +137,7 @@ where
           | (.tcons "bool" [], some (.tcons "int" []), none)
           | (.tcons "bool" [], none, some (.tcons "bool" []))
           | (.tcons "bool" [], some (.tcons "int" []), some (.tcons "bool" [])) =>
-            let (tb, Env, C) ← go C Env [(Stmt.block "$_loop_body" bss #[])] []
+            let (tb, Env, C) ← goBlock C Env bss []
             let s' := Stmt.loop conda.unresolved (mt.map LExpr.unresolved) (it.map LExpr.unresolved) tb md
             .ok (s', Env, C)
           | _ =>
@@ -177,8 +176,11 @@ where
             .error (errorWithSourceLoc e md)
 
       go C Env srest (s' :: acc)
-    termination_by Block.sizeOf ss
-    decreasing_by all_goals term_by_mem
+  goBlock (C : LContext CoreLParams) (Env : TEnv Visibility) (bss : Imperative.Block Core.Expression Core.Command) (acc : List Statement) :
+    Except DiagnosticModel (List Statement × TEnv Visibility × LContext CoreLParams) := do
+    let Env := Env.pushEmptyContext
+    let (ss', Env, C) ← go C Env bss acc
+    .ok (ss', Env.popContext, C)
 
 private def substOptionExpr (S : Subst) (oe : Option Expression.Expr) : Option Expression.Expr :=
   match oe with