Add B3 Verifier: SMT-based verification for B3 programs

JOSH_REVIEW_COMMENTS.md

@@ -0,0 +1,184 @@
+# Josh's Review Comments on PR #307
+
+**Reviewer:** @joscoh (Josh)  
+**Date:** January 15, 2026  
+**Status:** Pending response
+
+---
+
+## Comment 1: Use List.map instead of for loop ✅ DONE
+
+**File:** `Strata/Languages/B3/Verifier/Program.lean`  
+**Line:** 106  
+**Comment:**
+> I think it's nicer to have `let results := results ++ List.map .error conversionErrors`
+
+**Status:** ✅ Fixed
+
+**Change Applied:**
+```lean
+results := results ++ conversionErrors.map .error
+```
+
+**Commit:** (pending)
+
+---
+
+## Comment 2: Remove unnecessary mutable variable ✅ DONE
+
+**File:** `Strata/Languages/B3/Verifier/Program.lean`  
+**Line:** 94  
+**Comment:**
+> This does not need to be mutable.
+
+**Status:** ✅ Fixed
+
+**Change Applied:**
+```lean
+let initialState ← initVerificationState solver
+...
+let (state, conversionErrors) ← addDeclarationsAndAxioms initialState transformedProg
+```
+
+**Commit:** (pending)
+
+---
+
+## Comment 3: Remove duplicate section header ✅ DONE
+
+**File:** `Strata/Languages/B3/Verifier/Program.lean`  
+**Line:** 119  
+**Comment:**
+> Repeated section
+
+**Status:** ✅ Fixed
+
+**Change Applied:** Removed duplicate header.
+
+**Commit:** (pending)
+
+---
+
+## Comment 4: Remove unused section header ✅ DONE
+
+**File:** `Strata/Languages/B3/Verifier/State.lean`  
+**Line:** 63  
+**Comment:**
+> Is this section header used?
+
+**Status:** ✅ Fixed
+
+**Change Applied:** Removed unused "Verification State" header that was immediately followed by "Verification Context and Results" header.
+
+**Commit:** (pending)
+
+---
+
+## Comment 5: Use reverse list building pattern ✅ DONE
+
+**File:** `Strata/Languages/B3/Verifier/Program.lean`  
+**Line:** 202  
+**Comment:**
+> Again, it would be better to build the reverse list with `::` and reverse the whole thing at the end.
+
+**Status:** ✅ Fixed
+
+**Change Applied:**
+```lean
+let mut reportsRev := []
+...
+reportsRev := {procedureName := name, results := resultsWithDiag} :: reportsRev
+...
+return reportsRev.reverse
+```
+
+**Commit:** (pending)
+
+---
+
+## Comment 6: Same optimization for Statements.lean ✅ DONE
+
+**File:** `Strata/Languages/B3/Verifier/Statements.lean`  
+**Line:** 98  
+**Comment:**
+> Same as above
+
+**Status:** ✅ Fixed
+
+**Change Applied:** Used `::` and reverse pattern in both `statementToSMTWithoutDiagnosis` (Statements.lean) and `statementToSMT` (Diagnosis.lean).
+
+**Commit:** (pending)
+
+---
+
+## Comment 7: No partial evaluation in B3? ✅ RESPONDED
+
+**File:** `StrataTest/Languages/B3/Verifier/VerifierTests.lean`  
+**Line:** 485  
+**Comment:**
+> I take it from this test this is no B3 partial evaluation, right?
+
+**Status:** ✅ Clarified by user
+
+**Response:** User confirmed this is correct - B3 doesn't do partial evaluation, it translates directly to SMT terms and lets the SMT.Factory layer handle constant folding.
+
+---
+
+## Comment 8: Declaration ordering and dependencies ✅ RESPONDED
+
+**File:** `Strata/Languages/B3/Transform/FunctionToAxiom.lean`  
+**Line:** 154  
+**Comment:**
+> Makes sense, but it seems a little strange to me that getting things in the correct order is bound up with generating axioms for functions (with another function encoding, we would still need to make sure the order is consistent). And this doesn't even completely enforce the right order, since I don't think it deals with dependencies between e.g. two functions, one of which calls the other.
+
+**Status:** ✅ Clarified
+
+**Note:** The ordering is: types → function declarations → axioms → other. This is correct for SMT-LIB where sorts must come before functions, and function declarations before axioms. Function-to-function dependencies don't matter for declarations (only for axioms), and the current ordering handles this correctly.
+
+---
+
+## Comment 9: Remove bullet points from Formatter.lean docstring
+
+**File:** `Strata/Languages/B3/Verifier/Formatter.lean`  
+**Comment:**
+> I don't think we need these bullets here personally.
+
+**Current Code:**
+```lean
+This module uses `SMTDDM.toString` which translates SMT terms to the SMT dialect's
+AST and then uses the dialect's formatter to generate SMT-LIB strings. This approach:
+- Is more efficient than string interpolation
+- Produces direct, readable SMT-LIB output (no A-normal form)
+- Leverages the existing SMT dialect infrastructure
+- Ensures consistency with other SMT formatting in Strata
+```
+
+**Recommendation:** **Accept** - Simplify the docstring to be more concise without the bullet points.
+
+**Effort:** Trivial
+
+---
+
+## Comment 9: Remove bullet points from Formatter.lean docstring ✅ DONE
+
+**File:** `Strata/Languages/B3/Verifier/Formatter.lean`  
+**Comment:**
+> I don't think we need these bullets here personally.
+
+**Status:** ✅ Fixed
+
+**Change Applied:** Simplified docstring to remove bullet points, keeping just the essential description.
+
+**Commit:** (pending)
+
+---
+
+## Summary
+
+**Total Comments:** 9
+
+**Status:**
+- ✅ **Fixed:** 6 (Comments 1, 2, 3, 4, 5, 6, 9)
+- ✅ **Responded:** 2 (Comments 7, 8)
+
+**All comments addressed!**

Strata/DL/SMT/DDMTransform/Parse.lean

@@ -95,7 +95,10 @@ def specialCharsInSimpleSymbol := [
     ("caret", "^"),
     ("lt", "<"),
     ("gt", ">"),
-    ("at", "@")
+    ("at", "@"),
+    ("le", "<="),
+    ("ge", ">="),
+    ("implies", "=>")
   ]
 
 -- https://smt-lib.org/papers/smt-lib-reference-v2.7-r2025-07-07.pdf
@@ -159,7 +162,7 @@ category Symbol;
 op symbol (@[unwrap] s:SimpleSymbol) : Symbol => s;
 
 category Keyword;
-op kw_symbol (@[unwrap] s:SimpleSymbol) : Keyword => ":" s;
+op kw_symbol (@[unwrap] s:SimpleSymbol) : Keyword => ":" s:0;
 
 
 // 2. S-expressions
@@ -180,12 +183,12 @@ op sc_numeral_neg (@[unwrap] n:Num) : SpecConstant => "-" n:0;
 op sc_decimal_neg (@[unwrap] n:Decimal) : SpecConstant => "-" n:0;
 
 category SExpr;
-op se_spec_const (s:SpecConstant) : SExpr => s;
-op se_symbol (s:Symbol) : SExpr => s;
-op se_reserved (s:Reserved) : SExpr => s;
-op se_keyword (s:Keyword) : SExpr => s;
+op se_spec_const (s:SpecConstant) : SExpr => s:0;
+op se_symbol (s:Symbol) : SExpr => s:0;
+op se_reserved (s:Reserved) : SExpr => s:0;
+op se_keyword (s:Keyword) : SExpr => s:0;
 
-op se_ls (s:SpaceSepBy SExpr) : SExpr => "(" s ")";
+op se_ls (s:SpaceSepBy SExpr) : SExpr => "(" s:0 ")";
 
 
 category SMTIdentifier;
@@ -211,12 +214,12 @@ op smtsort_param (s:SMTIdentifier, @[nonempty] sl:SpaceSepBy SMTSort) : SMTSort
 
 // 5. Attributes
 category AttributeValue;
-op av_spec_constant (s:SpecConstant) : AttributeValue => s;
-op av_symbol (s:Symbol) : AttributeValue => s;
-op av_sel (s:Seq SExpr) : AttributeValue => "(" s ")";
+op av_spec_constant (s:SpecConstant) : AttributeValue => s:0;
+op av_symbol (s:Symbol) : AttributeValue => s:0;
+op av_sel (s:Seq SExpr) : AttributeValue => "(" s:0 ")";
 
 category Attribute;
-op att_kw (k:Keyword, av:Option AttributeValue) : Attribute => k av;
+op att_kw (k:Keyword, av:Option AttributeValue) : Attribute => k:0 " " av:0;
 
 
 // 6. Terms
@@ -239,18 +242,18 @@ op sorted_var (s:Symbol, so:SMTSort) : SortedVar => "(" s " " so ")";
 op spec_constant_term (sc:SpecConstant) : Term => sc;
 op qual_identifier (qi:QualIdentifier) : Term => qi;
 op qual_identifier_args (qi:QualIdentifier, @[nonempty] ts:SpaceSepBy Term) : Term =>
-  "(" qi " " ts ")";
+  "(" qi " " ts:0 ")";
 
 op let_smt (@[nonempty] vbps: SpaceSepBy ValBinding, t:Term) : Term =>
-  "(" "let" "(" vbps ")" t ")";
+  "(" "let " "(" vbps ")" t ")";
 op lambda_smt (@[nonempty] svs: SpaceSepBy SortedVar, t:Term) : Term =>
-  "(" "lambda" "(" svs ")" t ")";
+  "(" "lambda " "(" svs ")" t ")";
 op forall_smt (@[nonempty] svs: SpaceSepBy SortedVar, t:Term) : Term =>
-  "(" "forall" "(" svs ")" t ")";
+  "(" "forall " "(" svs ") " t ")";
 op exists_smt (@[nonempty] svs: SpaceSepBy SortedVar, t:Term) : Term =>
-  "(" "exists" "(" svs ")" t ")";
+  "(" "exists " "(" svs ") " t ")";
 op bang (t:Term, @[nonempty] attrs:SpaceSepBy Attribute) : Term =>
-  "(" "!" t " " attrs ")";
+  "(" "! " t:0 " " attrs:0 ")";
 
 
 // 7. Theories

Strata/DL/SMT/DDMTransform/Translate.lean

@@ -32,6 +32,9 @@ private def mkSimpleSymbol (s:String):SimpleSymbol SourceRange :=
     | "lt" => .simple_symbol_lt SourceRange.none
     | "gt" => .simple_symbol_gt SourceRange.none
     | "at" => .simple_symbol_at SourceRange.none
+    | "le" => .simple_symbol_le SourceRange.none
+    | "ge" => .simple_symbol_ge SourceRange.none
+    | "implies" => .simple_symbol_implies SourceRange.none
     | _ => panic! s!"Unknown simple symbol: {name}")
   | .none =>
     .simple_symbol_qid SourceRange.none (mkQualifiedIdent s)
@@ -110,6 +113,35 @@ private def translateFromTermType (t:SMT.TermType):
     else
       return .smtsort_param srnone (mkIdentifier id) (Ann.mk srnone argtys_array)
 
+-- Helper function to convert a SMTDDM.Term to SExpr for use in pattern attributes
+def termToSExpr (t : SMTDDM.Term SourceRange) : SMTDDM.SExpr SourceRange :=
+  let srnone := SourceRange.none
+  match t with
+  | .qual_identifier _ qi =>
+      match qi with
+      | .qi_ident _ iden =>
+          match iden with
+          | .iden_simple _ sym => .se_symbol srnone sym
+          | _ => .se_symbol srnone (.symbol srnone (.simple_symbol_qid srnone (mkQualifiedIdent "term")))
+      | _ => .se_symbol srnone (.symbol srnone (.simple_symbol_qid srnone (mkQualifiedIdent "term")))
+  | .qual_identifier_args _ qi args =>
+      -- Function application in pattern: convert to nested S-expr
+      let qiSExpr := match qi with
+        | .qi_ident _ iden =>
+            match iden with
+            | .iden_simple _ sym => SMTDDM.SExpr.se_symbol srnone sym
+            | _ => .se_symbol srnone (.symbol srnone (.simple_symbol_qid srnone (mkQualifiedIdent "fn")))
+        | _ => .se_symbol srnone (.symbol srnone (.simple_symbol_qid srnone (mkQualifiedIdent "fn")))
+      -- Convert args array to SExpr list
+      let argsSExpr := args.val.map termToSExpr
+      .se_ls srnone (Ann.mk srnone ((qiSExpr :: argsSExpr.toList).toArray))
+  | _ => .se_symbol srnone (.symbol srnone (.simple_symbol_qid srnone (mkQualifiedIdent "term")))
+  decreasing_by
+    cases args
+    rename_i hargs
+    have := Array.sizeOf_lt_of_mem hargs
+    simp_all; omega
+
 def translateFromTerm (t:SMT.Term): Except String (SMTDDM.Term SourceRange) := do
   let srnone := SourceRange.none
   match t with
@@ -126,7 +158,7 @@ def translateFromTerm (t:SMT.Term): Except String (SMTDDM.Term SourceRange) := d
     else
       return (.qual_identifier_args srnone
         (.qi_ident srnone (mkIdentifier op.mkName)) (Ann.mk srnone args_array))
-  | .quant qkind args _tr body =>
+  | .quant qkind args tr body =>
     let args_sorted:List (SMTDDM.SortedVar SourceRange) <-
       args.mapM
         (fun ⟨name,ty⟩ => do
@@ -137,11 +169,37 @@ def translateFromTerm (t:SMT.Term): Except String (SMTDDM.Term SourceRange) := d
       throw "empty quantifier"
     else
       let body <- translateFromTerm body
+
+      -- Handle triggers/patterns
+      let bodyWithPattern <-
+        match tr with
+        | .app .triggers triggerTerms .trigger =>
+          if triggerTerms.isEmpty then
+            -- No patterns - return body as-is
+            pure body
+          else
+            -- Convert each trigger term to a SMTDDM.Term, then to SExpr
+            let triggerDDMTerms <- triggerTerms.mapM translateFromTerm
+            let triggerSExprs := triggerDDMTerms.map termToSExpr
+
+            -- Create the :pattern attribute
+            -- av_sel wraps the SExprs in parens, so we pass the array directly
+            let patternAttr : SMTDDM.Attribute SourceRange :=
+              .att_kw srnone
+                (.kw_symbol srnone (mkSimpleSymbol "pattern"))
+                (Ann.mk srnone (some (.av_sel srnone (Ann.mk srnone triggerSExprs.toArray))))
+
+            -- Wrap body with bang operator and pattern attribute
+            pure (.bang srnone body (Ann.mk srnone #[patternAttr]))
+        | _ =>
+          -- Unexpected trigger format - return body as-is
+          pure body
+
       match qkind with
       | .all =>
-        return .forall_smt srnone (Ann.mk srnone args_array) body
+        return .forall_smt srnone (Ann.mk srnone args_array) bodyWithPattern
       | .exist =>
-        return .exists_smt srnone (Ann.mk srnone args_array) body
+        return .exists_smt srnone (Ann.mk srnone args_array) bodyWithPattern
 
 
 private def dummy_prg_for_toString :=

Strata/DL/SMT/Op.lean

@@ -246,7 +246,7 @@ def Op.mkName : Op → String
   | .not           => "not"
   | .and           => "and"
   | .or            => "or"
-  | .eq            => "eq"
+  | .eq            => "="
   | .ite           => "ite"
   | .implies       => "=>"
   | .distinct      => "distinct"