Classify division-by-zero checks as distinct property type

Strata/DL/Imperative/CmdEval.lean

@@ -18,7 +18,7 @@ public section
 /--
 Partial evaluator for an Imperative Command.
 -/
-def Cmd.eval [EC : EvalContext P S] (σ : S) (c : Cmd P) : Cmd P × S :=
+def Cmd.eval [BEq P.Ident] [EC : EvalContext P S] (σ : S) (c : Cmd P) : Cmd P × S :=
   match EC.lookupError σ with
   | some _ => (c, σ)
   | none =>
@@ -65,16 +65,19 @@ def Cmd.eval [EC : EvalContext P S] (σ : S) (c : Cmd P) : Cmd P × S :=
       let e := EC.eval σ e
       let assumptions := EC.getPathConditions σ
       let c' := .assert label e md
+      let propType := match md.getPropertyType with
+        | some s => if s == MetaData.divisionByZero then .divisionByZero else .assert
+        | none => .assert
       match EC.denoteBool e with
       | some true => -- Proved via evaluation.
-        (c', EC.deferObligation σ (ProofObligation.mk label .assert assumptions e md))
+        (c', EC.deferObligation σ (ProofObligation.mk label propType assumptions e md))
       | some false =>
         if assumptions.isEmpty then
           (c', EC.updateError σ (.AssertFail label e))
         else
-          (c', EC.deferObligation σ (ProofObligation.mk label .assert assumptions e md))
+          (c', EC.deferObligation σ (ProofObligation.mk label propType assumptions e md))
       | none =>
-        (c', EC.deferObligation σ (ProofObligation.mk label .assert assumptions e md))
+        (c', EC.deferObligation σ (ProofObligation.mk label propType assumptions e md))
 
     | .assume label e md =>
       let (e, σ) := EC.preprocess σ c e
@@ -99,7 +102,7 @@ def Cmd.eval [EC : EvalContext P S] (σ : S) (c : Cmd P) : Cmd P × S :=
 /--
 Partial evaluator for Imperative's Commands.
 -/
-def Cmds.eval [EvalContext P S] (σ : S) (cs : Cmds P) : Cmds P × S :=
+def Cmds.eval [BEq P.Ident] [EvalContext P S] (σ : S) (cs : Cmds P) : Cmds P × S :=
   match cs with
   | [] => ([], σ)
   | c :: crest =>

Strata/DL/Imperative/EvalContext.lean

@@ -72,12 +72,14 @@ def PathConditions.removeByNames (ps : PathConditions P) (names : List String) :
 inductive PropertyType where
   | cover
   | assert
+  | divisionByZero
   deriving Repr, DecidableEq
 
 instance : ToFormat PropertyType where
   format p := match p with
     | .cover => "cover"
     | .assert => "assert"
+    | .divisionByZero => "division by zero check"
 
 /--
 A proof obligation can be discharged by some backend solver or a dedicated

Strata/DL/Imperative/MetaData.lean

@@ -214,6 +214,20 @@ def MetaData.formatFileRangeD {P : PureExpr} [BEq P.Ident] (md : MetaData P) (fi
   | some fr => fr.format fileMap includeEnd?
   | none => f!""
 
+/-- Metadata field for property type classification (e.g., "divisionByZero"). -/
+def MetaData.propertyType : MetaDataElem.Field P := .label "propertyType"
+
+/-- Metadata value for division-by-zero property type classification. -/
+def MetaData.divisionByZero : String := "divisionByZero"
+
+/-- Read the property type classification from metadata, if present. -/
+def MetaData.getPropertyType {P : PureExpr} [BEq P.Ident] (md : MetaData P) : Option String :=
+  match md.findElem MetaData.propertyType with
+  | some elem => match elem.value with
+    | .msg s => some s
+    | _ => none
+  | none => none
+
 ---------------------------------------------------------------------
 
 end -- public section

Strata/Languages/Core/SarifOutput.lean

@@ -50,9 +50,16 @@ def extractLocation (files : Map Strata.Uri Lean.FileMap) (md : Imperative.MetaD
     pure { uri, startLine := startPos.line, startColumn := startPos.column }
   | _ => none
 
+/-- Convert PropertyType to a property classification string for SARIF output -/
+def propertyTypeToClassification : Imperative.PropertyType → String
+  | .divisionByZero => "division-by-zero"
+  | .cover => "cover"
+  | .assert => "assert"
+
 /-- Convert a VCResult to a SARIF Result -/
 def vcResultToSarifResult (files : Map Strata.Uri Lean.FileMap) (vcr : VCResult) : Strata.Sarif.Result :=
   let ruleId := vcr.obligation.label
+  let classification := propertyTypeToClassification vcr.obligation.property
   let level := outcomeToLevel vcr.result
   let messageText :=
     if vcr.isUnreachable then "Path is unreachable"
@@ -63,7 +70,7 @@ def vcResultToSarifResult (files : Map Strata.Uri Lean.FileMap) (vcr : VCResult)
     | some loc => #[locationToSarif loc]
     | none => #[]
 
-  { ruleId, level, message, locations }
+  { ruleId, level, message, locations, properties := { propertyType := classification } }
 
 /-- Convert VCResults to a SARIF document -/
 def vcResultsToSarif (files : Map Strata.Uri Lean.FileMap) (vcResults : VCResults) : Strata.Sarif.SarifDocument :=

Strata/Languages/Core/StatementEval.lean

@@ -341,7 +341,10 @@ private def createUnreachableAssertObligations
     Imperative.ProofObligations Expression :=
   asserts.toArray.map
     (fun (label, md) =>
-      (Imperative.ProofObligation.mk label .assert pathConditions (LExpr.true ()) md))
+      let propType := match md.getPropertyType with
+        | some s => if s == Imperative.MetaData.divisionByZero then .divisionByZero else .assert
+        | _ => .assert
+      (Imperative.ProofObligation.mk label propType pathConditions (LExpr.true ()) md))
 
 /--
 Substitute free variables in an expression with their current values from the environment,

Strata/Languages/Core/Verifier.lean

@@ -270,7 +270,7 @@ def preprocessObligation (obligation : ProofObligation Expression) (p : Program)
       return (obligation, some result)
     else
       return (obligation, none)
-  | .assert =>
+  | .assert | .divisionByZero =>
     if obligation.obligation.isTrue && !needsReachCheck then
       -- We don't need the SMT solver if PE (partial evaluation) is enough to
       -- reduce the consequent to true. Skip the shortcut when reachCheck is

Strata/Transform/PrecondElim.lean

@@ -45,18 +45,29 @@ def wfProcName (name : String) : String := s!"{name}{wfSuffix}"
 
 /-! ## Collecting assertions from expressions -/
 
+/-- Classify a function name into a property type for SARIF reporting. -/
+private def classifyPrecondition (funcName : String) : Option String :=
+  if funcName.startsWith "Int.SafeDiv" || funcName.startsWith "Int.SafeMod" then
+    some Imperative.MetaData.divisionByZero
+  else
+    none
+
 /--
 Given a Factory and an expression, collect all partial function call
 precondition obligations and return them as `assert` statements.
-The metadata from the original statement is attached to the generated assertions.
+The metadata from the original statement is attached to the generated assertions,
+with property type classification added when applicable.
 -/
 def collectPrecondAsserts (F : @Lambda.Factory CoreLParams) (e : Expression.Expr)
 (labelPrefix : String) (md : Imperative.MetaData Expression := .empty)
 : List Statement :=
   let wfObs := Lambda.collectWFObligations F e
   wfObs.mapIdx fun idx ob =>
+    let md' := match classifyPrecondition ob.funcName with
+      | some pt => md.pushElem Imperative.MetaData.propertyType (.msg pt)
+      | none => md
     Statement.assert
-    s!"{labelPrefix}_calls_{ob.funcName}_{idx}" ob.obligation md
+    s!"{labelPrefix}_calls_{ob.funcName}_{idx}" ob.obligation md'
 
 /--
 Collect assertions for all expressions in a command.

Strata/Util/Sarif.lean

@@ -83,13 +83,21 @@ instance : FromJson Level where
     | "error" => pure .error
     | _ => throw s!"Invalid SARIF level: {s}"
 
+/-- SARIF property bag for tool-specific properties -/
+structure PropertyBag where
+  /-- Strata-specific classification of the property being checked -/
+  propertyType : String := "assert"
+  deriving Repr, ToJson, FromJson, DecidableEq
+
 /-- SARIF result representing a single verification result -/
 structure Result where
   /-- Stable identifier of the rule that was evaluated to produce the result --/
   ruleId : String
   level : Level
   message : Message
   locations : Array SarifLocation := #[]
+  /-- Tool-specific properties (SARIF property bag) -/
+  properties : PropertyBag := {}
   deriving Repr, ToJson, FromJson, DecidableEq
 
 instance : Inhabited Result where

StrataTest/Languages/Core/Examples/FunctionPreconditions.lean

@@ -27,15 +27,15 @@ info: [Strata.Core] Type checking succeeded.
 
 VCs:
 Label: safeDiv_body_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Assumptions:
 precond_safeDiv_0: !($__y1 == 0)
 Obligation:
 !($__y1 == 0)
 
 ---
 info: Obligation: safeDiv_body_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Result: ✅ pass
 -/
 #guard_msgs in
@@ -159,14 +159,14 @@ info: [Strata.Core] Type checking succeeded.
 
 VCs:
 Label: foo_precond_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Assumptions:
 precond_foo_0: $__y1 > 0
 Obligation:
 !($__y1 == 0)
 
 Label: foo_body_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Assumptions:
 precond_foo_0: $__y1 > 0
 precond_foo_1: $__x0 / $__y1 > 0
@@ -175,11 +175,11 @@ Obligation:
 
 ---
 info: Obligation: foo_precond_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Result: ✅ pass
 
 Obligation: foo_body_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Result: ✅ pass
 -/
 #guard_msgs in
@@ -205,15 +205,15 @@ info: [Strata.Core] Type checking succeeded.
 
 VCs:
 Label: doubleDiv_body_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Assumptions:
 precond_doubleDiv_0: !($__y1 == 0)
 precond_doubleDiv_1: !($__z2 == 0)
 Obligation:
 !($__z2 == 0)
 
 Label: doubleDiv_body_calls_Int.SafeDiv_1
-Property: assert
+Property: division by zero check
 Assumptions:
 precond_doubleDiv_0: !($__y1 == 0)
 precond_doubleDiv_1: !($__z2 == 0)
@@ -223,11 +223,11 @@ Obligation:
 ---
 info:
 Obligation: doubleDiv_body_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Result: ✅ pass
 
 Obligation: doubleDiv_body_calls_Int.SafeDiv_1
-Property: assert
+Property: division by zero check
 Result: ✅ pass
 -/
 #guard_msgs in
@@ -250,14 +250,14 @@ info: [Strata.Core] Type checking succeeded.
 
 VCs:
 Label: badDiv_body_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Obligation:
 false
 
 
 
 Result: Obligation: badDiv_body_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Result: ❌ fail
 
 
@@ -273,7 +273,7 @@ function badDiv (x : int) : int {
 ---
 info:
 Obligation: badDiv_body_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Result: ❌ fail
 -/
 #guard_msgs in
@@ -297,13 +297,13 @@ info: [Strata.Core] Type checking succeeded.
 
 VCs:
 Label: init_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Obligation:
 true
 
 ---
 info: Obligation: init_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Result: ✅ pass
 -/
 #guard_msgs in
@@ -331,15 +331,15 @@ info: [Strata.Core] Type checking succeeded.
 
 VCs:
 Label: set_z_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Assumptions:
 <label_ite_cond_true: (~Int.Gt a #0)>: $__a0 > 0
 Obligation:
 !($__a0 == 0)
 
 ---
 info: Obligation: set_z_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Result: ✅ pass
 -/
 #guard_msgs in
@@ -368,7 +368,7 @@ info: [Strata.Core] Type checking succeeded.
 
 VCs:
 Label: safeDiv_body_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Assumptions:
 precond_safeDiv_0: !($__y1 == 0)
 Obligation:
@@ -383,7 +383,7 @@ Obligation:
 
 ---
 info: Obligation: safeDiv_body_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Result: ✅ pass
 
 Obligation: init_calls_safeDiv_0
@@ -416,7 +416,7 @@ info: [Strata.Core] Type checking succeeded.
 
 VCs:
 Label: safeDiv_body_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Assumptions:
 precond_safeDiv_0: !($__y1 == 0)
 Obligation:
@@ -431,7 +431,7 @@ forall __q0 : int :: __q0 > 0 ==> !(__q0 == 0)
 
 ---
 info: Obligation: safeDiv_body_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Result: ✅ pass
 
 Obligation: allPositiveDiv_body_calls_safeDiv_0
@@ -512,7 +512,7 @@ info: [Strata.Core] Type checking succeeded.
 
 VCs:
 Label: loop_guard_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Assumptions:
 test_requires_0: !($__n0 == 0)
 Obligation:
@@ -539,7 +539,7 @@ $__i1 + 1 >= 0
 ---
 info:
 Obligation: loop_guard_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Result: ✅ pass
 
 Obligation: entry_invariant_0_0