Remove unused big-step semantics of Imperative, comment sorry-ed lemmas transitively (#806)

This pull request

- Removes the unused big-step semantics of Imperative
- Renames Strata/DL/Imperative/StmtSemanticsSmallStep.lean to
Strata/DL/Imperative/StmtSemantics.lean, and
- Comments out sorry-ed lemmas as well as other theorems that
transitively use them, removing the sorry related warnings.

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

Author: aqjune-aws

Strata/DL/Imperative/CFGSemantics.lean

@@ -6,7 +6,7 @@
 import Strata.DL.Imperative.BasicBlock
 import Strata.DL.Imperative.Cmd
 import Strata.DL.Imperative.CmdSemantics
-import Strata.DL.Imperative.StmtSemanticsSmallStep
+import Strata.DL.Imperative.StmtSemantics
 import Strata.DL.Util.Relations
 
 ---------------------------------------------------------------------

Strata/DL/Imperative/Imperative.lean

@@ -12,7 +12,7 @@ public import Strata.DL.Imperative.MetaData
 public import Strata.DL.Imperative.CmdEval
 public import Strata.DL.Imperative.CmdType
 public import Strata.DL.Imperative.CmdSemantics
-public import Strata.DL.Imperative.StmtSemanticsSmallStep
+public import Strata.DL.Imperative.StmtSemantics
 
 public import Strata.DL.Imperative.KleeneStmt
 public import Strata.DL.Imperative.KleeneStmtSemantics

Strata/DL/Imperative/KleeneStmtSemantics.lean

@@ -6,7 +6,7 @@
 module
 
 public import Strata.DL.Imperative.KleeneStmt
-public import Strata.DL.Imperative.StmtSemanticsSmallStep
+public import Strata.DL.Imperative.StmtSemantics
 
 ---------------------------------------------------------------------
 

Strata/DL/Imperative/SemanticsProps.lean

@@ -7,8 +7,8 @@ module
 
 public import Strata.DL.Imperative.CmdSemantics
 import all Strata.DL.Imperative.CmdSemantics
-public import Strata.DL.Imperative.StmtSemanticsSmallStep
-import all Strata.DL.Imperative.StmtSemanticsSmallStep
+public import Strata.DL.Imperative.StmtSemantics
+import all Strata.DL.Imperative.StmtSemantics
 import all Strata.DL.Imperative.Cmd
 
 namespace Imperative
@@ -190,7 +190,7 @@ theorem EvalStmtsSmall_hasFailure_irrel
   ∃ ρ₂', EvalStmtsSmall P EvalCmd extendEval ρ₂ ss ρ₂' ∧
     ρ₂'.store = ρ'.store ∧ ρ₂'.eval = ρ'.eval := by
   intro Heval ρ₂ Hstore Heval_eq
-  -- Reuse the simulation-based proof from StmtSemanticsSmallStep
+  -- Reuse the simulation-based proof from StmtSemantics
   -- smallStep_hasFailure_irrel works on .stmt configs; we need .stmts
   -- Use the same simulation technique directly
   suffices ∀ (c₁ c₂ : Config P CmdT),