Small-step Imperative semantics: loop/ite exit handling and invariant checking (#1052)

- Small-step `.exit` semantics: According to the previous small-step
statement, `{ loop .. { exit ; } print "a"; } print "b" }` was exiting
the outerblock as well and made this print "b", not "ab". This patch
makes exit without destination block only escape the loop. For if { exit
} else { exit }, this is consistently applied.

- Loop invariants are now checked by `step_loop_{,nondet_}{enter,exit}`:
each invariant must evaluate to `tt`/`ff`, and any `ff` result ORs a
fresh `hasInvFailure` flag into the env's cumulative `hasFailure`,
mirroring how `step_cmd` threads assert failures. (refer to:
Strata/DL/Imperative/StmtSemantics.lean)

- `Stmt.loop` invariants are now labeled pairs `List (String × P.Expr)`
(distinct labels per invariant, like assert labels). Downstream
frontends, backends, and passive-encoding transforms are updated to
carry the labels through. (refer to: Strata/DL/Imperative/Stmt.lean,
Strata/DL/Imperative/StmtSemantics.lean)

- The Core syntax is extended to allow a label to invariants.
```
  while (i < n)
    invariant [test]: 0 <= i
  {
    i := (i + 1);
  }

```

*Issue #, if available:*

*Description of changes:*


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: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: aqjune-aws

Strata/Backends/CBMC/GOTO/CoreToGOTOPipeline.lean

@@ -80,7 +80,8 @@ private partial def unwrapCmdExt
     .ok (.ite (c.map (renameExpr rn)) t' e' md)
   | .loop g m i body md => do
     let body' ← body.mapM (unwrapCmdExt rn)
-    .ok (.loop (g.map (renameExpr rn)) (m.map (renameExpr rn)) (i.map (renameExpr rn)) body' md)
+    .ok (.loop (g.map (renameExpr rn)) (m.map (renameExpr rn))
+      (i.map (fun (l, e) => (l, renameExpr rn e))) body' md)
   | .exit l md => .ok (.exit l md)
   | .funcDecl _d _md =>
     .error f!"[unwrapCmdExt] Unexpected funcDecl; should have been lifted by collectFuncDecls."
@@ -216,7 +217,7 @@ private partial def coreStmtsToGoto
             Imperative.emitCondGoto (CProverGOTO.Expr.not guard_expr) srcLoc trans
           let trans ← coreStmtsToGoto Env pname rn body trans
           let mut backGuard := CProverGOTO.Expr.true
-          for inv in invariants do
+          for (_, inv) in invariants do
             let inv_expr ← toExpr (renameExpr rn inv)
             backGuard := backGuard.setNamedField "#spec_loop_invariant" inv_expr
           match measure with

Strata/DL/Imperative/KleeneSemanticsProps.lean

@@ -0,0 +1,72 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+public import Strata.DL.Imperative.KleeneStmtSemantics
+import all Strata.DL.Imperative.CmdSemantics
+import all Strata.DL.Util.Relations
+
+/-! # Properties of Kleene (nondeterministic) small-step semantics
+
+Generic helpers for `StepKleene` / `StepKleeneStar` that are independent
+of any particular program transformation. -/
+
+namespace Imperative
+
+public section
+
+variable {P : PureExpr} [HasFvar P] [HasBool P] [HasNot P] [HasVal P] [HasBoolVal P]
+
+/-! ## Env helpers -/
+
+omit [HasFvar P] [HasVal P] [HasBool P] [HasNot P] in
+theorem assume_env_eq (ρ : Env P) :
+    ({ ρ with store := ρ.store, hasFailure := ρ.hasFailure || false } : Env P) = ρ := by
+  cases ρ; simp [Bool.or_false]
+
+omit [HasFvar P] [HasNot P] in
+theorem eval_tt_is_tt
+    (δ : SemanticEval P) (σ : SemanticStore P)
+    (hwfv : WellFormedSemanticEvalVal δ) :
+    δ σ HasBool.tt = some HasBool.tt :=
+  hwfv.2 HasBool.tt σ HasBoolVal.bool_is_val.1
+
+/-! ## Kleene small-step helpers -/
+
+omit [HasVal P] [HasBoolVal P] in
+theorem kleene_seq_inner_star
+    (inner inner' : KleeneConfig P (Cmd P)) (s2 : KleeneStmt P (Cmd P))
+    (h : StepKleeneStar P (EvalCmd P) inner inner') :
+    StepKleeneStar P (EvalCmd P) (.seq inner s2) (.seq inner' s2) := by
+  induction h with
+  | refl => exact .refl _
+  | step _ mid _ hstep _ ih => exact .step _ _ _ (.step_seq_inner hstep) ih
+
+omit [HasVal P] [HasBoolVal P] in
+theorem kleene_seq_terminal
+    (s1 s2 : KleeneStmt P (Cmd P)) (ρ ρ₁ ρ' : Env P)
+    (h1 : StepKleeneStar P (EvalCmd P) (.stmt s1 ρ) (.terminal ρ₁))
+    (h2 : StepKleeneStar P (EvalCmd P) (.stmt s2 ρ₁) (.terminal ρ')) :
+    StepKleeneStar P (EvalCmd P) (.stmt (.seq s1 s2) ρ) (.terminal ρ') :=
+  .step _ _ _ .step_seq (ReflTrans_Transitive _ _ _ _
+    (ReflTrans_Transitive _ _ _ _ (kleene_seq_inner_star _ _ s2 h1)
+      (.step _ _ _ .step_seq_done (.refl _))) h2)
+
+omit [HasVal P] [HasBoolVal P] in
+theorem kleene_assume_terminal
+    {label : String} {expr : P.Expr} {md : MetaData P} {ρ₀ : Env P}
+    (hcond : ρ₀.eval ρ₀.store expr = some HasBool.tt)
+    (hwfb : WellFormedSemanticEvalBool ρ₀.eval) :
+    StepKleeneStar P (EvalCmd P)
+      (.stmt (.cmd (.assume label expr md)) ρ₀) (.terminal ρ₀) := by
+  have raw : StepKleeneStar P (EvalCmd P)
+      (.stmt (.cmd (.assume label expr md)) ρ₀)
+      (.terminal { ρ₀ with store := ρ₀.store, hasFailure := ρ₀.hasFailure || false }) :=
+    .step _ _ _ (.step_cmd (EvalCmd.eval_assume hcond hwfb)) (.refl _)
+  rwa [assume_env_eq] at raw
+
+end -- public section
+end Imperative

Strata/DL/Imperative/SemanticsProps.lean

@@ -119,10 +119,14 @@ private theorem step_hasFailure_monotone
   | step_ite_false _ _ => exact hf
   | step_ite_nondet_true => exact hf
   | step_ite_nondet_false => exact hf
-  | step_loop_enter _ _ => exact hf
-  | step_loop_exit _ _ => exact hf
-  | step_loop_nondet_enter => exact hf
-  | step_loop_nondet_exit => exact hf
+  | step_loop_enter _ _ _ _ =>
+    simp [Config.getEnv]; left; exact hf
+  | step_loop_exit _ _ _ _ =>
+    simp [Config.getEnv]; left; exact hf
+  | step_loop_nondet_enter _ _ =>
+    simp [Config.getEnv]; left; exact hf
+  | step_loop_nondet_exit _ _ =>
+    simp [Config.getEnv]; left; exact hf
   | step_exit => exact hf
   | step_funcDecl => simp [Config.getEnv]; exact hf
   | step_typeDecl => exact hf
@@ -169,6 +173,18 @@ theorem EvalStmtsSmall_hasFailure_monotone
   | refl => exact hf
   | step _ _ _ hstep _ ih => exact ih (step_hasFailure_monotone hstep hf)
 
+theorem StepStmtStar_hasFailure_monotone
+  {P : PureExpr} {CmdT : Type} {EvalCmd : EvalCmdParam P CmdT}
+  {extendEval : ExtendEval P}
+  [HasBool P] [HasNot P]
+  {c c' : Config P CmdT}
+  (hstar : StepStmtStar P EvalCmd extendEval c c')
+  (hf : c.getEnv.hasFailure = true) :
+  c'.getEnv.hasFailure = true := by
+  induction hstar with
+  | refl => exact hf
+  | step _ _ _ hstep _ ih => exact ih (step_hasFailure_monotone hstep hf)
+
 theorem EvalStmtSmall_hasFailure_irrel
   {P : PureExpr} {CmdT : Type} {EvalCmd : EvalCmdParam P CmdT}
   {extendEval : ExtendEval P}

Strata/DL/Imperative/Stmt.lean

@@ -37,9 +37,11 @@ inductive Stmt (P : PureExpr) (Cmd : Type) : Type where
   is chosen non-deterministically. -/
   | ite      (cond : ExprOrNondet P)  (thenb : List (Stmt P Cmd)) (elseb : List (Stmt P Cmd)) (md : MetaData P)
   /-- An iterated execution statement. Includes an optional measure (for
-  termination) and invariants. When `guard` is `.nondet`, the loop iterates
-  a non-deterministic number of times. -/
-  | loop     (guard : ExprOrNondet P) (measure : Option P.Expr) (invariants : List P.Expr)
+  termination) and labeled invariants. When `guard` is `.nondet`, the loop iterates
+  a non-deterministic number of times. Each invariant carries a label string
+  (expected to be distinct, like assert labels do). -/
+  | loop     (guard : ExprOrNondet P) (measure : Option P.Expr)
+             (invariants : List (String × P.Expr))
              (body : List (Stmt P Cmd)) (md : MetaData P)
   /-- An exit statement that transfers control out of the nearest enclosing
   block with the given label. If no label is provided, exits the nearest
@@ -74,7 +76,7 @@ def Stmt.inductionOn {P : PureExpr} {Cmd : Type}
       (∀ s, s ∈ thenb → motive s) →
       (∀ s, s ∈ elseb → motive s) →
       motive (Stmt.ite cond thenb elseb md))
-    (loop_case : ∀ (guard : ExprOrNondet P) (measure : Option P.Expr) (invariant : List P.Expr)
+    (loop_case : ∀ (guard : ExprOrNondet P) (measure : Option P.Expr) (invariant : List (String × P.Expr))
       (body : List (Stmt P Cmd)) (md : MetaData P),
       (∀ s, s ∈ body → motive s) →
       motive (Stmt.loop guard measure invariant body md))
@@ -307,7 +309,11 @@ def formatStmt (P : PureExpr) (s : Stmt P C)
 
   | .loop guard measure invariant body md =>
       let body := formatBlock P body
-      let beforeBody := nestD f!"{line}{guard}{line}({measure}){line}{invariant}"
+      -- Format each labeled invariant as `[lbl]: expr` (unlabeled ones just as `expr`).
+      let invParts : List Format := invariant.map fun (l, e) =>
+        if l.isEmpty then f!"{e}" else f!"[{l}]: {e}"
+      let invFmt : Format := f!"[{Format.joinSep invParts f!", "}]"
+      let beforeBody := nestD f!"{line}{guard}{line}({measure}){line}{invFmt}"
       let children := group f!"{beforeBody}{line}{body}"
       f!"{md}while{children}"
   | .exit label md => match label with
@@ -344,25 +350,29 @@ instance [ToFormat P.Ident] [ToFormat P.Expr] [ToFormat P.Ty] [ToFormat C]
 by an enclosing `block` — either within `s` itself or with a label in
 `labels` (representing blocks that enclose `s` externally).
 
-When `s.exitsCoveredByBlocks []`, execution of `s` can never produce `.exiting`. -/
+When `s.exitsCoveredByBlocks []`, execution of `s` can never produce `.exiting`.
 
-@[expose] def Stmt.exitsCoveredByBlocks : List String → Stmt P CmdT → Prop
+The labels have type `Option String` (not `String`) so that `exit` without
+destination block label can be considered as covered even when it is surrounded
+by unlabeled blocks (`[None]`). -/
+
+@[expose] def Stmt.exitsCoveredByBlocks : List (Option String) → Stmt P CmdT → Prop
   | _, .cmd _ => True
-  | labels, .block l ss _ => Block.exitsCoveredByBlocks (l :: labels) ss
+  | labels, .block l ss _ => Block.exitsCoveredByBlocks (.some l :: labels) ss
   | labels, .ite _ tss ess _ => Block.exitsCoveredByBlocks labels tss ∧ Block.exitsCoveredByBlocks labels ess
   | labels, .loop _ _ _ body _ => Block.exitsCoveredByBlocks labels body
   | labels, .exit none _ => labels.length > 0
-  | labels, .exit (some l) _ => l ∈ labels
+  | labels, .exit (some l) _ => .some l ∈ labels
   | _, .funcDecl _ _ => True
   | _, .typeDecl _ _ => True
 where
-  Block.exitsCoveredByBlocks : List String → List (Stmt P CmdT) → Prop
+  Block.exitsCoveredByBlocks : List (Option String) → List (Stmt P CmdT) → Prop
     | _, [] => True
     | labels, s :: ss => Stmt.exitsCoveredByBlocks labels s ∧ Block.exitsCoveredByBlocks labels ss
 
 theorem block_exitsCoveredByBlocks_append
     {P : PureExpr} {CmdT : Type}
-    (labels : List String) (ss₁ ss₂ : List (Stmt P CmdT))
+    (labels : List (Option String)) (ss₁ ss₂ : List (Stmt P CmdT))
     (h₁ : Stmt.exitsCoveredByBlocks.Block.exitsCoveredByBlocks labels ss₁)
     (h₂ : Stmt.exitsCoveredByBlocks.Block.exitsCoveredByBlocks labels ss₂) :
     Stmt.exitsCoveredByBlocks.Block.exitsCoveredByBlocks labels (ss₁ ++ ss₂) := by
@@ -374,7 +384,7 @@ theorem block_exitsCoveredByBlocks_append
     can only help. -/
 theorem exitsCoveredByBlocks_weaken
     {P : PureExpr} {CmdT : Type}
-    (labels₁ labels₂ : List String)
+    (labels₁ labels₂ : List (Option String))
     (hsub : ∀ l, l ∈ labels₁ → l ∈ labels₂) :
     (∀ (s : Stmt P CmdT),
       s.exitsCoveredByBlocks labels₁ → s.exitsCoveredByBlocks labels₂) ∧
@@ -399,8 +409,8 @@ theorem exitsCoveredByBlocks_weaken
   | cmd _ => intros; trivial
   | block l ss _ ih =>
     intro labels₁ labels₂ hsub h
-    show Stmt.exitsCoveredByBlocks.Block.exitsCoveredByBlocks (l :: labels₂) ss
-    exact ih (l :: labels₁) (l :: labels₂)
+    show Stmt.exitsCoveredByBlocks.Block.exitsCoveredByBlocks (.some l :: labels₂) ss
+    exact ih (.some l :: labels₁) (.some l :: labels₂)
       (fun x hx => by cases hx with
         | head => exact .head _
         | tail _ hm => exact .tail _ (hsub x hm))
@@ -418,7 +428,7 @@ theorem exitsCoveredByBlocks_weaken
       show labels₂.length > 0
       exact List.length_pos_iff_exists_mem.mpr
         (let ⟨x, hx⟩ := List.length_pos_iff_exists_mem.mp h; ⟨x, hsub x hx⟩)
-    | some l => exact hsub l h
+    | some l => exact hsub (.some l) h
   | funcDecl _ _ => intros; trivial
   | typeDecl _ _ => intros; trivial
   | nil => intros; trivial
@@ -430,7 +440,7 @@ theorem exitsCoveredByBlocks_weaken
     for any labels (since `.cmd` has no exit statements). -/
 theorem all_cmd_exitsCoveredByBlocks
     {P : PureExpr} {CmdT : Type}
-    (labels : List String) (ss : List (Stmt P CmdT))
+    (labels : List (Option String)) (ss : List (Stmt P CmdT))
     (h : ∀ s ∈ ss, ∃ c, s = Stmt.cmd c) :
     Stmt.exitsCoveredByBlocks.Block.exitsCoveredByBlocks labels ss := by
   induction ss with