From ed5408cba763c4be280cb9b8346e541167475225 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 4 Mar 2026 11:26:42 +0000
Subject: [PATCH 1/4] Classify division-by-zero checks as distinct property
 type

Extend PropertyType with a divisionByZero variant so that verification
results from safe division/modulo preconditions are distinguishable from
regular assertions. PrecondElim attaches a propertyType metadata tag
based on the function name (Int.SafeDiv*, Int.SafeMod*), which CmdEval
reads when creating proof obligations. The classification propagates to
both text output (Property: division by zero check) and SARIF output
(kind: division-by-zero).

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 Strata/DL/Imperative/CmdEval.lean             | 12 +++--
 Strata/DL/Imperative/EvalContext.lean         |  2 +
 Strata/DL/Imperative/MetaData.lean            | 11 +++++
 Strata/Languages/Core/SarifOutput.lean        |  9 +++-
 Strata/Languages/Core/Verifier.lean           |  2 +-
 Strata/Transform/PrecondElim.lean             | 15 +++++-
 Strata/Util/Sarif.lean                        |  2 +
 .../Core/Examples/FunctionPreconditions.lean  | 46 +++++++++----------
 StrataTest/Languages/Core/Examples/Loops.lean |  8 ++--
 .../Core/Examples/NoFilterWFProc.lean         |  4 +-
 .../Languages/Core/SarifOutputTests.lean      | 10 ++--
 11 files changed, 80 insertions(+), 41 deletions(-)

diff --git a/Strata/DL/Imperative/CmdEval.lean b/Strata/DL/Imperative/CmdEval.lean
index ee242884f..94e9db8a6 100644
--- a/Strata/DL/Imperative/CmdEval.lean
+++ b/Strata/DL/Imperative/CmdEval.lean
@@ -64,16 +64,22 @@ 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.find? (fun elem =>
+          match elem.fld, elem.value with
+          | .label "propertyType", .msg "divisionByZero" => true
+          | _, _ => false) with
+        | some _ => PropertyType.divisionByZero
+        | none => PropertyType.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
diff --git a/Strata/DL/Imperative/EvalContext.lean b/Strata/DL/Imperative/EvalContext.lean
index 218c3bea8..98e2e9a49 100644
--- a/Strata/DL/Imperative/EvalContext.lean
+++ b/Strata/DL/Imperative/EvalContext.lean
@@ -71,12 +71,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
diff --git a/Strata/DL/Imperative/MetaData.lean b/Strata/DL/Imperative/MetaData.lean
index 03facd1d8..6f899def9 100644
--- a/Strata/DL/Imperative/MetaData.lean
+++ b/Strata/DL/Imperative/MetaData.lean
@@ -211,6 +211,17 @@ 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"
+
+/-- 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 Imperative
diff --git a/Strata/Languages/Core/SarifOutput.lean b/Strata/Languages/Core/SarifOutput.lean
index 94f38d5e2..cadf5fa12 100644
--- a/Strata/Languages/Core/SarifOutput.lean
+++ b/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 SARIF-friendly rule ID prefix -/
+def propertyTypeToRuleKind : 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 kind := propertyTypeToRuleKind 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, kind, level, message, locations }
 
 /-- Convert VCResults to a SARIF document -/
 def vcResultsToSarif (files : Map Strata.Uri Lean.FileMap) (vcResults : VCResults) : Strata.Sarif.SarifDocument :=
diff --git a/Strata/Languages/Core/Verifier.lean b/Strata/Languages/Core/Verifier.lean
index 7f1e4e392..4db18a747 100644
--- a/Strata/Languages/Core/Verifier.lean
+++ b/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
diff --git a/Strata/Transform/PrecondElim.lean b/Strata/Transform/PrecondElim.lean
index f67c89c22..d4a23b13b 100644
--- a/Strata/Transform/PrecondElim.lean
+++ b/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 "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.
diff --git a/Strata/Util/Sarif.lean b/Strata/Util/Sarif.lean
index 20809fb54..3f70646a3 100644
--- a/Strata/Util/Sarif.lean
+++ b/Strata/Util/Sarif.lean
@@ -87,6 +87,8 @@ instance : FromJson Level where
 structure Result where
   /-- Stable identifier of the rule that was evaluated to produce the result --/
   ruleId : String
+  /-- Classification of the property being checked (e.g., "division-by-zero", "assert") -/
+  kind : String := "assert"
   level : Level
   message : Message
   locations : Array SarifLocation := #[]
diff --git a/StrataTest/Languages/Core/Examples/FunctionPreconditions.lean b/StrataTest/Languages/Core/Examples/FunctionPreconditions.lean
index 60e2d935c..3dda12717 100644
--- a/StrataTest/Languages/Core/Examples/FunctionPreconditions.lean
+++ b/StrataTest/Languages/Core/Examples/FunctionPreconditions.lean
@@ -27,7 +27,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:
@@ -35,7 +35,7 @@ Obligation:
 
 ---
 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,7 +205,7 @@ 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)
@@ -213,7 +213,7 @@ 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,7 +331,7 @@ 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:
@@ -339,7 +339,7 @@ Obligation:
 
 ---
 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
diff --git a/StrataTest/Languages/Core/Examples/Loops.lean b/StrataTest/Languages/Core/Examples/Loops.lean
index ab11b0d6c..7893e1307 100644
--- a/StrataTest/Languages/Core/Examples/Loops.lean
+++ b/StrataTest/Languages/Core/Examples/Loops.lean
@@ -39,14 +39,14 @@ info: [Strata.Core] Type checking succeeded.
 
 VCs:
 Label: sum_post_sum_ensures_1_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Assumptions:
 sum_requires_0: $__n0 >= 0
 Obligation:
 true
 
 Label: loop_invariant_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Assumptions:
 sum_requires_0: $__n2 >= 0
 Obligation:
@@ -132,11 +132,11 @@ if 0 < $__n2 then $__s8 else 0 == $__n2 * ($__n2 + 1) / 2
 ---
 info:
 Obligation: sum_post_sum_ensures_1_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Result: ✅ pass
 
 Obligation: loop_invariant_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Result: ✅ pass
 
 Obligation: entry_invariant_0_0
diff --git a/StrataTest/Languages/Core/Examples/NoFilterWFProc.lean b/StrataTest/Languages/Core/Examples/NoFilterWFProc.lean
index c3f14289a..765c6bacc 100644
--- a/StrataTest/Languages/Core/Examples/NoFilterWFProc.lean
+++ b/StrataTest/Languages/Core/Examples/NoFilterWFProc.lean
@@ -33,11 +33,11 @@ spec {
 /--
 info:
 Obligation: P_post_result_ok_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Result: ✅ pass
 
 Obligation: set_r_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Result: ✅ pass
 
 Obligation: result_ok
diff --git a/StrataTest/Languages/Core/SarifOutputTests.lean b/StrataTest/Languages/Core/SarifOutputTests.lean
index b5eb1b5eb..eb26daa3c 100644
--- a/StrataTest/Languages/Core/SarifOutputTests.lean
+++ b/StrataTest/Languages/Core/SarifOutputTests.lean
@@ -272,7 +272,7 @@ def makeVCResult (label : String) (outcome : Outcome)
   let sarif := vcResultsToSarif files vcResults
   Strata.Sarif.toJsonString sarif
 
-/-- info: "{\"runs\":[{\"results\":[{\"level\":\"none\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/pass.st\"},\"region\":{\"startColumn\":0,\"startLine\":1}}}],\"message\":{\"text\":\"Verification succeeded\"},\"ruleId\":\"test_pass\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
+/-- info: "{\"runs\":[{\"results\":[{\"kind\":\"assert\",\"level\":\"none\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/pass.st\"},\"region\":{\"startColumn\":0,\"startLine\":1}}}],\"message\":{\"text\":\"Verification succeeded\"},\"ruleId\":\"test_pass\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
 #guard_msgs in
 #eval
   let md := makeMetadata "/test/pass.st" 10 5
@@ -281,7 +281,7 @@ def makeVCResult (label : String) (outcome : Outcome)
   let sarif := vcResultsToSarif files vcResults
   Strata.Sarif.toJsonString sarif
 
-/-- info: "{\"runs\":[{\"results\":[{\"level\":\"error\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/fail.st\"},\"region\":{\"startColumn\":0,\"startLine\":1}}}],\"message\":{\"text\":\"Verification failed\"},\"ruleId\":\"test_fail\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
+/-- info: "{\"runs\":[{\"results\":[{\"kind\":\"assert\",\"level\":\"error\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/fail.st\"},\"region\":{\"startColumn\":0,\"startLine\":1}}}],\"message\":{\"text\":\"Verification failed\"},\"ruleId\":\"test_fail\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
 #guard_msgs in
 #eval
   let md := makeMetadata "/test/fail.st" 20 15
@@ -290,7 +290,7 @@ def makeVCResult (label : String) (outcome : Outcome)
   let sarif := vcResultsToSarif files vcResults
   Strata.Sarif.toJsonString sarif
 
-/-- info: "{\"runs\":[{\"results\":[{\"level\":\"warning\",\"locations\":[],\"message\":{\"text\":\"Verification result unknown (solver timeout or incomplete)\"},\"ruleId\":\"test_unknown\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
+/-- info: "{\"runs\":[{\"results\":[{\"kind\":\"assert\",\"level\":\"warning\",\"locations\":[],\"message\":{\"text\":\"Verification result unknown (solver timeout or incomplete)\"},\"ruleId\":\"test_unknown\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
 #guard_msgs in
 #eval
   let files := makeFilesMap "/test/file.st"
@@ -298,7 +298,7 @@ def makeVCResult (label : String) (outcome : Outcome)
   let sarif := vcResultsToSarif files vcResults
   Strata.Sarif.toJsonString sarif
 
-/-- info: "{\"runs\":[{\"results\":[{\"level\":\"error\",\"locations\":[],\"message\":{\"text\":\"Verification error: timeout\"},\"ruleId\":\"test_error\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
+/-- info: "{\"runs\":[{\"results\":[{\"kind\":\"assert\",\"level\":\"error\",\"locations\":[],\"message\":{\"text\":\"Verification error: timeout\"},\"ruleId\":\"test_error\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
 #guard_msgs in
 #eval
   let files := makeFilesMap "/test/file.st"
@@ -306,7 +306,7 @@ def makeVCResult (label : String) (outcome : Outcome)
   let sarif := vcResultsToSarif files vcResults
   Strata.Sarif.toJsonString sarif
 
-/-- info: "{\"runs\":[{\"results\":[{\"level\":\"none\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/multi.st\"},\"region\":{\"startColumn\":0,\"startLine\":1}}}],\"message\":{\"text\":\"Verification succeeded\"},\"ruleId\":\"obligation1\"},{\"level\":\"error\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/multi.st\"},\"region\":{\"startColumn\":0,\"startLine\":1}}}],\"message\":{\"text\":\"Verification failed\"},\"ruleId\":\"obligation2\"},{\"level\":\"warning\",\"locations\":[],\"message\":{\"text\":\"Verification result unknown (solver timeout or incomplete)\"},\"ruleId\":\"obligation3\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
+/-- info: "{\"runs\":[{\"results\":[{\"kind\":\"assert\",\"level\":\"none\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/multi.st\"},\"region\":{\"startColumn\":0,\"startLine\":1}}}],\"message\":{\"text\":\"Verification succeeded\"},\"ruleId\":\"obligation1\"},{\"kind\":\"assert\",\"level\":\"error\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/multi.st\"},\"region\":{\"startColumn\":0,\"startLine\":1}}}],\"message\":{\"text\":\"Verification failed\"},\"ruleId\":\"obligation2\"},{\"kind\":\"assert\",\"level\":\"warning\",\"locations\":[],\"message\":{\"text\":\"Verification result unknown (solver timeout or incomplete)\"},\"ruleId\":\"obligation3\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
 #guard_msgs in
 #eval
   let md1 := makeMetadata "/test/multi.st" 5 1

From 905308ba07a8e5779314d762929dc5b51440ca97 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 4 Mar 2026 21:47:19 +0000
Subject: [PATCH 2/4] Use SARIF property bag instead of non-standard kind field

Move the property classification from the non-standard 'kind' field to
a SARIF-compliant 'properties' bag with a 'propertyType' entry. Rename
propertyTypeToRuleKind to propertyTypeToClassification to reflect its
updated purpose.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 Strata/Languages/Core/SarifOutput.lean          |  8 ++++----
 Strata/Util/Sarif.lean                          | 10 ++++++++--
 StrataTest/Languages/Core/SarifOutputTests.lean | 10 +++++-----
 3 files changed, 17 insertions(+), 11 deletions(-)

diff --git a/Strata/Languages/Core/SarifOutput.lean b/Strata/Languages/Core/SarifOutput.lean
index cadf5fa12..3104ec8d7 100644
--- a/Strata/Languages/Core/SarifOutput.lean
+++ b/Strata/Languages/Core/SarifOutput.lean
@@ -50,8 +50,8 @@ def extractLocation (files : Map Strata.Uri Lean.FileMap) (md : Imperative.MetaD
     pure { uri, startLine := startPos.line, startColumn := startPos.column }
   | _ => none
 
-/-- Convert PropertyType to a SARIF-friendly rule ID prefix -/
-def propertyTypeToRuleKind : Imperative.PropertyType → String
+/-- Convert PropertyType to a property classification string for SARIF output -/
+def propertyTypeToClassification : Imperative.PropertyType → String
   | .divisionByZero => "division-by-zero"
   | .cover => "cover"
   | .assert => "assert"
@@ -59,7 +59,7 @@ def propertyTypeToRuleKind : Imperative.PropertyType → String
 /-- 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 kind := propertyTypeToRuleKind vcr.obligation.property
+  let classification := propertyTypeToClassification vcr.obligation.property
   let level := outcomeToLevel vcr.result
   let messageText :=
     if vcr.isUnreachable then "Path is unreachable"
@@ -70,7 +70,7 @@ def vcResultToSarifResult (files : Map Strata.Uri Lean.FileMap) (vcr : VCResult)
     | some loc => #[locationToSarif loc]
     | none => #[]
 
-  { ruleId, kind, 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 :=
diff --git a/Strata/Util/Sarif.lean b/Strata/Util/Sarif.lean
index 3f70646a3..54271f1cc 100644
--- a/Strata/Util/Sarif.lean
+++ b/Strata/Util/Sarif.lean
@@ -83,15 +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
-  /-- Classification of the property being checked (e.g., "division-by-zero", "assert") -/
-  kind : String := "assert"
   level : Level
   message : Message
   locations : Array SarifLocation := #[]
+  /-- Tool-specific properties (SARIF property bag) -/
+  properties : PropertyBag := {}
   deriving Repr, ToJson, FromJson, DecidableEq
 
 instance : Inhabited Result where
diff --git a/StrataTest/Languages/Core/SarifOutputTests.lean b/StrataTest/Languages/Core/SarifOutputTests.lean
index eb26daa3c..4f8a4d6bf 100644
--- a/StrataTest/Languages/Core/SarifOutputTests.lean
+++ b/StrataTest/Languages/Core/SarifOutputTests.lean
@@ -272,7 +272,7 @@ def makeVCResult (label : String) (outcome : Outcome)
   let sarif := vcResultsToSarif files vcResults
   Strata.Sarif.toJsonString sarif
 
-/-- info: "{\"runs\":[{\"results\":[{\"kind\":\"assert\",\"level\":\"none\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/pass.st\"},\"region\":{\"startColumn\":0,\"startLine\":1}}}],\"message\":{\"text\":\"Verification succeeded\"},\"ruleId\":\"test_pass\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
+/-- info: "{\"runs\":[{\"results\":[{\"level\":\"none\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/pass.st\"},\"region\":{\"startColumn\":0,\"startLine\":1}}}],\"message\":{\"text\":\"Verification succeeded\"},\"properties\":{\"propertyType\":\"assert\"},\"ruleId\":\"test_pass\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
 #guard_msgs in
 #eval
   let md := makeMetadata "/test/pass.st" 10 5
@@ -281,7 +281,7 @@ def makeVCResult (label : String) (outcome : Outcome)
   let sarif := vcResultsToSarif files vcResults
   Strata.Sarif.toJsonString sarif
 
-/-- info: "{\"runs\":[{\"results\":[{\"kind\":\"assert\",\"level\":\"error\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/fail.st\"},\"region\":{\"startColumn\":0,\"startLine\":1}}}],\"message\":{\"text\":\"Verification failed\"},\"ruleId\":\"test_fail\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
+/-- info: "{\"runs\":[{\"results\":[{\"level\":\"error\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/fail.st\"},\"region\":{\"startColumn\":0,\"startLine\":1}}}],\"message\":{\"text\":\"Verification failed\"},\"properties\":{\"propertyType\":\"assert\"},\"ruleId\":\"test_fail\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
 #guard_msgs in
 #eval
   let md := makeMetadata "/test/fail.st" 20 15
@@ -290,7 +290,7 @@ def makeVCResult (label : String) (outcome : Outcome)
   let sarif := vcResultsToSarif files vcResults
   Strata.Sarif.toJsonString sarif
 
-/-- info: "{\"runs\":[{\"results\":[{\"kind\":\"assert\",\"level\":\"warning\",\"locations\":[],\"message\":{\"text\":\"Verification result unknown (solver timeout or incomplete)\"},\"ruleId\":\"test_unknown\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
+/-- info: "{\"runs\":[{\"results\":[{\"level\":\"warning\",\"locations\":[],\"message\":{\"text\":\"Verification result unknown (solver timeout or incomplete)\"},\"properties\":{\"propertyType\":\"assert\"},\"ruleId\":\"test_unknown\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
 #guard_msgs in
 #eval
   let files := makeFilesMap "/test/file.st"
@@ -298,7 +298,7 @@ def makeVCResult (label : String) (outcome : Outcome)
   let sarif := vcResultsToSarif files vcResults
   Strata.Sarif.toJsonString sarif
 
-/-- info: "{\"runs\":[{\"results\":[{\"kind\":\"assert\",\"level\":\"error\",\"locations\":[],\"message\":{\"text\":\"Verification error: timeout\"},\"ruleId\":\"test_error\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
+/-- info: "{\"runs\":[{\"results\":[{\"level\":\"error\",\"locations\":[],\"message\":{\"text\":\"Verification error: timeout\"},\"properties\":{\"propertyType\":\"assert\"},\"ruleId\":\"test_error\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
 #guard_msgs in
 #eval
   let files := makeFilesMap "/test/file.st"
@@ -306,7 +306,7 @@ def makeVCResult (label : String) (outcome : Outcome)
   let sarif := vcResultsToSarif files vcResults
   Strata.Sarif.toJsonString sarif
 
-/-- info: "{\"runs\":[{\"results\":[{\"kind\":\"assert\",\"level\":\"none\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/multi.st\"},\"region\":{\"startColumn\":0,\"startLine\":1}}}],\"message\":{\"text\":\"Verification succeeded\"},\"ruleId\":\"obligation1\"},{\"kind\":\"assert\",\"level\":\"error\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/multi.st\"},\"region\":{\"startColumn\":0,\"startLine\":1}}}],\"message\":{\"text\":\"Verification failed\"},\"ruleId\":\"obligation2\"},{\"kind\":\"assert\",\"level\":\"warning\",\"locations\":[],\"message\":{\"text\":\"Verification result unknown (solver timeout or incomplete)\"},\"ruleId\":\"obligation3\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
+/-- info: "{\"runs\":[{\"results\":[{\"level\":\"none\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/multi.st\"},\"region\":{\"startColumn\":0,\"startLine\":1}}}],\"message\":{\"text\":\"Verification succeeded\"},\"properties\":{\"propertyType\":\"assert\"},\"ruleId\":\"obligation1\"},{\"level\":\"error\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/multi.st\"},\"region\":{\"startColumn\":0,\"startLine\":1}}}],\"message\":{\"text\":\"Verification failed\"},\"properties\":{\"propertyType\":\"assert\"},\"ruleId\":\"obligation2\"},{\"level\":\"warning\",\"locations\":[],\"message\":{\"text\":\"Verification result unknown (solver timeout or incomplete)\"},\"properties\":{\"propertyType\":\"assert\"},\"ruleId\":\"obligation3\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
 #guard_msgs in
 #eval
   let md1 := makeMetadata "/test/multi.st" 5 1

From 4c788472827c8b58b5560ce33f16c46625e0936b Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 4 Mar 2026 21:48:52 +0000
Subject: [PATCH 3/4] Decode property type from metadata for unreachable
 assertions

Use MetaData.getPropertyType in createUnreachableAssertObligations
instead of hardcoding PropertyType.assert, so that unreachable
division-by-zero checks retain their property classification.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 Strata/Languages/Core/StatementEval.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/Strata/Languages/Core/StatementEval.lean b/Strata/Languages/Core/StatementEval.lean
index 47cd4c53a..8e849b023 100644
--- a/Strata/Languages/Core/StatementEval.lean
+++ b/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 "divisionByZero" => .divisionByZero
+        | _ => .assert
+      (Imperative.ProofObligation.mk label propType pathConditions (LExpr.true ()) md))
 
 /--
 Substitute free variables in an expression with their current values from the environment,

From 7469fcff0044ab340c566c5c3aec8c56640cf994 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 6 Mar 2026 13:04:16 +0100
Subject: [PATCH 4/4] Replace hard-coded property type strings with MetaData
 constants

Add MetaData.divisionByZero constant and use MetaData.getPropertyType
accessor consistently across CmdEval, StatementEval, and PrecondElim,
eliminating magic strings for property type classification.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 Strata/DL/Imperative/CmdEval.lean        | 13 +++++--------
 Strata/DL/Imperative/MetaData.lean       |  3 +++
 Strata/Languages/Core/StatementEval.lean |  2 +-
 Strata/Transform/PrecondElim.lean        |  2 +-
 4 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/Strata/DL/Imperative/CmdEval.lean b/Strata/DL/Imperative/CmdEval.lean
index 94e9db8a6..8836a3f17 100644
--- a/Strata/DL/Imperative/CmdEval.lean
+++ b/Strata/DL/Imperative/CmdEval.lean
@@ -17,7 +17,7 @@ open Std (ToFormat Format format)
 /--
 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 =>
@@ -64,12 +64,9 @@ 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.find? (fun elem =>
-          match elem.fld, elem.value with
-          | .label "propertyType", .msg "divisionByZero" => true
-          | _, _ => false) with
-        | some _ => PropertyType.divisionByZero
-        | none => PropertyType.assert
+      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 propType assumptions e md))
@@ -104,7 +101,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 =>
diff --git a/Strata/DL/Imperative/MetaData.lean b/Strata/DL/Imperative/MetaData.lean
index 6f899def9..b39535fd2 100644
--- a/Strata/DL/Imperative/MetaData.lean
+++ b/Strata/DL/Imperative/MetaData.lean
@@ -214,6 +214,9 @@ def MetaData.formatFileRangeD {P : PureExpr} [BEq P.Ident] (md : MetaData P) (fi
 /-- 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
diff --git a/Strata/Languages/Core/StatementEval.lean b/Strata/Languages/Core/StatementEval.lean
index 8e849b023..68bc7dfbd 100644
--- a/Strata/Languages/Core/StatementEval.lean
+++ b/Strata/Languages/Core/StatementEval.lean
@@ -342,7 +342,7 @@ private def createUnreachableAssertObligations
   asserts.toArray.map
     (fun (label, md) =>
       let propType := match md.getPropertyType with
-        | some "divisionByZero" => .divisionByZero
+        | some s => if s == Imperative.MetaData.divisionByZero then .divisionByZero else .assert
         | _ => .assert
       (Imperative.ProofObligation.mk label propType pathConditions (LExpr.true ()) md))
 
diff --git a/Strata/Transform/PrecondElim.lean b/Strata/Transform/PrecondElim.lean
index d4a23b13b..0a3520166 100644
--- a/Strata/Transform/PrecondElim.lean
+++ b/Strata/Transform/PrecondElim.lean
@@ -48,7 +48,7 @@ def wfProcName (name : String) : String := s!"{name}{wfSuffix}"
 /-- 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 "divisionByZero"
+    some Imperative.MetaData.divisionByZero
   else
     none