diff --git a/JOSH_REVIEW_COMMENTS.md b/JOSH_REVIEW_COMMENTS.md new file mode 100644 index 00000000..56672466 --- /dev/null +++ b/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!** diff --git a/Strata/DL/SMT/DDMTransform/Parse.lean b/Strata/DL/SMT/DDMTransform/Parse.lean index 20128a44..a1baba4b 100644 --- a/Strata/DL/SMT/DDMTransform/Parse.lean +++ b/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 diff --git a/Strata/DL/SMT/DDMTransform/Translate.lean b/Strata/DL/SMT/DDMTransform/Translate.lean index f4bad69d..ddd34c7d 100644 --- a/Strata/DL/SMT/DDMTransform/Translate.lean +++ b/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 := diff --git a/Strata/DL/SMT/Op.lean b/Strata/DL/SMT/Op.lean index 8b53f719..de9d6c89 100644 --- a/Strata/DL/SMT/Op.lean +++ b/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" diff --git a/Strata/Languages/B3/DDMTransform/DefinitionAST.lean b/Strata/Languages/B3/DDMTransform/DefinitionAST.lean index 8ab2de8a..d5b77946 100644 --- a/Strata/Languages/B3/DDMTransform/DefinitionAST.lean +++ b/Strata/Languages/B3/DDMTransform/DefinitionAST.lean @@ -299,7 +299,7 @@ def Statement.mapMetadata [Inhabited N] (f : M → N) (s: Statement M) : Stateme -- Unlike List and Array, Option.map does not use `attach` by default for wf proofs ⟨f elseB.ann, elseB.val.attach.map (fun x => Statement.mapMetadata f x.1)⟩ | .ifCase m cases => .ifCase (f m) ⟨f cases.ann, cases.val.map (fun o => - match ho: o with + match _: o with | .oneIfCase m cond body => .oneIfCase (f m) (Expression.mapMetadata f cond) (Statement.mapMetadata f body))⟩ | .loop m invariants body => .loop (f m) ⟨f invariants.ann, invariants.val.map (Expression.mapMetadata f)⟩ (Statement.mapMetadata f body) @@ -374,4 +374,25 @@ def Decl.toUnit [Inhabited (Expression Unit)] (d : Decl M) : Decl Unit := def Program.toUnit [Inhabited (Expression Unit)] (p : Program M) : Program Unit := p.mapMetadata (fun _ => ()) +/-- Extract metadata from any B3 statement -/ +def Statement.metadata : Statement M → M + | .check m _ => m + | .assert m _ => m + | .assume m _ => m + | .reach m _ => m + | .blockStmt m _ => m + | .probe m _ => m + | .varDecl m _ _ _ _ => m + | .assign m _ _ => m + | .reinit m _ => m + | .ifStmt m _ _ _ => m + | .ifCase m _ => m + | .choose m _ => m + | .loop m _ _ => m + | .labeledStmt m _ _ => m + | .exit m _ => m + | .returnStmt m => m + | .aForall m _ _ _ => m + | .call m _ _ => m + end B3AST diff --git a/Strata/Languages/B3/Transform/FunctionToAxiom.lean b/Strata/Languages/B3/Transform/FunctionToAxiom.lean new file mode 100644 index 00000000..b722c707 --- /dev/null +++ b/Strata/Languages/B3/Transform/FunctionToAxiom.lean @@ -0,0 +1,156 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Languages.B3.DDMTransform.DefinitionAST + +/-! +# Function-to-Axiom Transformation + +Transforms B3 programs by splitting function definitions into declarations and axioms. + +While SMT-LIB 2.6 provides `define-fun-rec` for mutually recursive definitions, +we use quantified axioms for broader solver compatibility and to maintain consistency +with our verification approach. By converting function bodies to axioms with quantifiers, +we enable verification of programs with mutually recursive functions across different +SMT solvers. + +TODO: Add config option to use `define-fun` for non-recursive functions instead of +quantified axioms. This could improve solver performance for simple function definitions. + +## Example: Simple Function + +Input: +``` +function abs(x : int) : int { + if x >= 0 then x else -x +} +``` + +Output: +``` +function abs(x : int) : int + +axiom forall x : int pattern abs(x) abs(x) == (if x >= 0 then x else -x) +``` + +## Example: Mutually Recursive Functions + +Input: +``` +function isEven(n : int) : int { + if n == 0 then 1 else isOdd(n - 1) +} +function isOdd(n : int) : int { + if n == 0 then 0 else isEven(n - 1) +} +``` + +Output: +``` +function isEven(n : int) : int +function isOdd(n : int) : int + +axiom forall n : int pattern isEven(n) isEven(n) == (if n == 0 then 1 else isOdd(n - 1)) +axiom forall n : int pattern isOdd(n) isOdd(n) == (if n == 0 then 0 else isEven(n - 1)) +``` + +## Example: Function with Precondition + +Input: +``` +function sqrt(x : int) : int + when x >= 0 +{ + ... +} +``` + +Output: +``` +function sqrt(x : int) : int + +axiom forall x : int pattern sqrt(x) (x >= 0) ==> (sqrt(x) == ...) +``` +-/ + +namespace Strata.B3.Transform + +open Strata.B3AST + +def transformFunctionDecl (decl : B3AST.Decl α) : Option (B3AST.Decl α × B3AST.Decl α) := + match decl with + | .function _m name params resultType tag body => + match body.val with + | some bodyAnn => + match bodyAnn with + | FunctionBody.functionBody m whens bodyExpr => + let funcDecl := B3AST.Decl.function m name params resultType tag (Ann.mk body.ann none) + let paramList := params.val.toList + let funcCallArgs : Array (Expression α) := + params.val.mapIdx (fun i _param => Expression.id m i) + let funcCall := Expression.functionCall m name ⟨m, funcCallArgs⟩ + let equality := Expression.binaryOp m (BinaryOp.eq m) funcCall bodyExpr + let axiomBody := + if whens.val.isEmpty then + equality + else + let whenExprs := whens.val.toList.filterMap (fun w => + match w with | When.when _m cond => some cond) + let whenConj := match whenExprs with + | [] => Expression.literal whens.ann (Literal.boolLit whens.ann true) + | first :: rest => rest.foldl (fun acc e => + Expression.binaryOp whens.ann (BinaryOp.and whens.ann) acc e + ) first + Expression.binaryOp whens.ann (BinaryOp.implies whens.ann) whenConj equality + -- Create pattern with function call + let pattern := Pattern.pattern m ⟨m, #[funcCall]⟩ + let axiomExpr := paramList.foldr (fun param body => + match param with + | FParameter.fParameter _m _inj paramName paramTy => + let varDecl := VarDecl.quantVarDecl m paramName paramTy + Expression.quantifierExpr m + (QuantifierKind.forall m) + ⟨m, #[varDecl]⟩ ⟨m, #[pattern]⟩ body + ) axiomBody + let axiomDecl := Decl.axiom m ⟨m, #[]⟩ axiomExpr + some (funcDecl, axiomDecl) + | none => none + | _ => none + +def functionToAxiom (prog : B3AST.Program α) : B3AST.Program α := + match prog with + | Program.program m decls => + Id.run do + let mut typeDeclsRev : List (B3AST.Decl α) := [] + let mut funcDeclsRev : List (B3AST.Decl α) := [] + let mut funcAxiomsRev : List (B3AST.Decl α) := [] + let mut otherDeclsRev : List (B3AST.Decl α) := [] + + for decl in decls.val.toList do + match decl with + | .typeDecl _ _ | .tagger _ _ _ => + typeDeclsRev := decl :: typeDeclsRev + | .function _ _ _ _ _ body => + match body.val with + | some bodyAnn => + match bodyAnn with + | FunctionBody.functionBody _ _ _ => + match transformFunctionDecl decl with + | some (funcDecl, axiomDecl) => + funcDeclsRev := funcDecl :: funcDeclsRev + funcAxiomsRev := axiomDecl :: funcAxiomsRev + | none => otherDeclsRev := decl :: otherDeclsRev + | none => + funcDeclsRev := decl :: funcDeclsRev + | .axiom _ _ _ => + funcAxiomsRev := decl :: funcAxiomsRev + | _ => + otherDeclsRev := decl :: otherDeclsRev + + let finalDecls := typeDeclsRev.reverse ++ funcDeclsRev.reverse ++ funcAxiomsRev.reverse ++ otherDeclsRev.reverse + return Program.program m ⟨decls.ann, finalDecls.toArray⟩ + +end Strata.B3.Transform diff --git a/Strata/Languages/B3/Verifier.lean b/Strata/Languages/B3/Verifier.lean new file mode 100644 index 00000000..c2ac8b2c --- /dev/null +++ b/Strata/Languages/B3/Verifier.lean @@ -0,0 +1,128 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Languages.B3.Verifier.Expression +import Strata.Languages.B3.Verifier.Formatter +import Strata.Languages.B3.Verifier.State +import Strata.Languages.B3.Verifier.Program +import Strata.Languages.B3.Verifier.Diagnosis + +open Strata +open Strata.B3.Verifier +open Strata.SMT + +/-! +# B3 Verifier + +Converts B3 programs to SMT and verifies them using SMT solvers. + +## Architecture Overview + +``` +B3 Program (CST) + ↓ + Parse (DDM) + ↓ + B3 AST (de Bruijn indices) + ↓ +FunctionToAxiom Transform + ↓ + B3 AST (declarations + axioms) + ↓ +expressionToSMT (Conversion) + ↓ + SMT Terms + ↓ +formatTermDirect (Formatter) + ↓ + SMT-LIB strings + ↓ + SMT Solver (e.g., Z3/CVC5) + ↓ + Results (proved/counterexample/unknown) + ↓ +Diagnosis (if failed) +``` + +## API Choice + +Use `programToSMT` for automatic diagnosis (recommended) - provides detailed error analysis. +Use `programToSMTWithoutDiagnosis` for faster verification without diagnosis - returns raw results. + +## Usage +-/ + +-- Example: Verify a simple B3 program (meta to avoid including in production) +-- This is not a test, it only demonstrates the end-to-end API +meta def exampleVerification : IO Unit := do + -- Parse B3 program using DDM syntax + let ddmProgram : Strata.Program := #strata program B3CST; + function f(x : int) : int { x + 1 } + procedure test() { + check 8 == 8 && f(5) == 7 + } + #end + + -- For parsing from files, use: parseStrataProgramFromDialect dialects "B3CST" "file.b3cst.st" + + let b3AST : B3AST.Program SourceRange ← match programToB3AST ddmProgram with + | .ok ast => pure ast + | .error msg => throw (IO.userError s!"Failed to parse: {msg}") + + -- Create solver and verify + let solver : Solver ← createInteractiveSolver "cvc5" + let reports : List ProcedureReport ← programToSMT b3AST solver + -- Don't call exit in tests - let solver terminate naturally + + -- Destructure results to show types (self-documenting) + let [report] ← pure reports | throw (IO.userError "Expected one procedure") + let _procedureName : String := report.procedureName + let results : List (VerificationReport × Option DiagnosisResult) := report.results + + let [(verificationReport, diagnosisOpt)] ← pure results | throw (IO.userError "Expected one result") + + let analyseVerificationReport (verificationReport: VerificationReport) : IO Unit := + do + let context : VerificationContext := verificationReport.context + let result : VerificationResult := verificationReport.result + let _model : Option String := verificationReport.model + + let _decl : B3AST.Decl SourceRange := context.decl + let _stmt : B3AST.Statement SourceRange := context.stmt + let pathCondition : List (B3AST.Expression SourceRange) := context.pathCondition + + -- Interpret verification result (merged error and success cases) + match result with + | .error .counterexample => IO.println "✗ Counterexample found (assertion may not hold)" + | .error .unknown => IO.println "✗ Unknown" + | .error .refuted => IO.println "✗ Refuted (proved false/unreachable)" + | .success .verified => IO.println "✓ Verified (proved)" + | .success .reachable => IO.println "✓ Reachable/Satisfiable" + | .success .reachabilityUnknown => IO.println "✓ Reachability unknown" + + -- Print path condition if present + if !pathCondition.isEmpty then + IO.println " Path condition:" + for expr in pathCondition do + IO.println s!" {B3.Verifier.formatExpression ddmProgram expr B3.ToCSTContext.empty}" + + IO.println s!"Statement: {B3.Verifier.formatStatement ddmProgram verificationReport.context.stmt B3.ToCSTContext.empty}" + analyseVerificationReport verificationReport + + let (.some diagnosis) ← pure diagnosisOpt | throw (IO.userError "Expected a diagnosis") + + -- Interpret diagnosis (if available) + let diagnosedFailures : List DiagnosedFailure := diagnosis.diagnosedFailures + IO.println s!" Found {diagnosedFailures.length} diagnosed failures" + + for failure in diagnosedFailures do + let expression : B3AST.Expression SourceRange := failure.expression + IO.println s!"Failing expression: {B3.Verifier.formatExpression ddmProgram expression B3.ToCSTContext.empty}" + analyseVerificationReport failure.report + + pure () + +-- See StrataTest/Languages/B3/Verifier/VerifierTests.lean for test of this example. diff --git a/Strata/Languages/B3/Verifier/Diagnosis.lean b/Strata/Languages/B3/Verifier/Diagnosis.lean new file mode 100644 index 00000000..9f59ccff --- /dev/null +++ b/Strata/Languages/B3/Verifier/Diagnosis.lean @@ -0,0 +1,193 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Languages.B3.Verifier.State +import Strata.Languages.B3.Verifier.Expression +import Strata.Languages.B3.Verifier.Statements + +/-! +# Verification Diagnosis Strategies + +Interactive debugging strategies for failed verifications. + +When a verification fails, these strategies help identify the root cause by: +- Splitting conjunctions to find which conjunct fails +- Inlining definitions +- Simplifying expressions +-/ + +namespace Strata.B3.Verifier + +open Strata.SMT + +--------------------------------------------------------------------- +-- Pure Helper Functions +--------------------------------------------------------------------- + +/-- Extract conjunction operands if expression is a conjunction, otherwise return none -/ +def splitConjunction (expr : B3AST.Expression SourceRange) : Option (B3AST.Expression SourceRange × B3AST.Expression SourceRange) := + match expr with + | .binaryOp _ (.and _) lhs rhs => some (lhs, rhs) + | _ => none + +/-- Determine if diagnosis should stop early based on check type and failure status -/ +def shouldStopDiagnosis (isReachCheck : Bool) (isProvablyFalse : Bool) : Bool := + isProvablyFalse || isReachCheck + +/-- Upgrade verification result to refuted if provably false -/ +def upgradeToRefutedIfNeeded (result : VerificationReport) (isProvablyFalse : Bool) : VerificationReport := + if isProvablyFalse then + { result with result := .error .refuted } + else + result + +/-- Automatically diagnose a failed check to find root cause. + +For proof checks (check/assert): Recursively splits conjunctions to find all atomic failures. +When checking RHS, assumes LHS holds to provide context-aware diagnosis. + +For reachability checks (reach): Stops after finding first unreachable LHS conjunct, +since all subsequent conjuncts are trivially unreachable if LHS is unreachable. +-/ +partial def diagnoseFailureGeneric + (isReachCheck : Bool) + (state : B3VerificationState) + (expr : B3AST.Expression SourceRange) + (sourceDecl : B3AST.Decl SourceRange) + (sourceStmt : B3AST.Statement SourceRange) : IO DiagnosisResult := do + let convResult := expressionToSMT ConversionContext.empty expr + + -- If there are conversion errors, return early + if !convResult.errors.isEmpty then + let vctx : VerificationContext := { decl := sourceDecl, stmt := sourceStmt, pathCondition := state.pathCondition } + let dummyResult : VerificationReport := { + context := vctx + result := .error .unknown + model := none + } + return { originalCheck := dummyResult, diagnosedFailures := [] } + + -- Determine check function based on check type + let checkFn := if isReachCheck then reach else prove + let isFailure := fun r => r.isError + + let vctx : VerificationContext := { decl := sourceDecl, stmt := sourceStmt, pathCondition := state.pathCondition } + let originalResult ← checkFn state convResult.term vctx + + if !isFailure originalResult.result then + return { originalCheck := originalResult, diagnosedFailures := [] } + + let mut diagnosements := [] + + -- Helper to diagnose a single conjunct + let diagnoseConjunct (expr : B3AST.Expression SourceRange) (convResult : ConversionResult SourceRange) + (checkState : B3VerificationState) (vctx : VerificationContext) : IO (List DiagnosedFailure) := do + let result ← checkFn checkState convResult.term vctx + if isFailure result.result then + -- Check if provably false (not just unprovable) + let _ ← push checkState + let runCheck : SolverM Decision := do + Solver.assert (formatTermDirect convResult.term) + Solver.checkSat [] + let decision ← runCheck.run checkState.smtState.solver + let _ ← pop checkState + let isProvablyFalse := decision == .unsat + + -- Recursively diagnose + let diag ← diagnoseFailureGeneric isReachCheck checkState expr sourceDecl sourceStmt + if diag.diagnosedFailures.isEmpty then + -- Atomic failure - upgrade to refuted if provably false + let finalResult := upgradeToRefutedIfNeeded result isProvablyFalse + return [{ expression := expr, report := finalResult }] + else + -- Has sub-failures - return those + return diag.diagnosedFailures + else + return [] + + -- Strategy: Pattern match on conjunctions and recursively diagnose + match expr with + | .binaryOp _ (.and _) lhs rhs => + let lhsConv := expressionToSMT ConversionContext.empty lhs + if lhsConv.errors.isEmpty then + let lhsFailures ← diagnoseConjunct lhs lhsConv state vctx + diagnosements := diagnosements ++ lhsFailures + + -- Stop early if needed (provably false or reachability check) + if !lhsFailures.isEmpty then + let hasProvablyFalse := lhsFailures.any (fun f => + match f.report.result with | .error .refuted => true | _ => false) + if shouldStopDiagnosis isReachCheck hasProvablyFalse then + return { originalCheck := originalResult, diagnosedFailures := diagnosements } + + -- Check right conjunct assuming left conjunct holds + let rhsConv := expressionToSMT ConversionContext.empty rhs + if lhsConv.errors.isEmpty && rhsConv.errors.isEmpty then + -- Add lhs as assumption when checking rhs + let stateForRhs ← addPathCondition state lhs lhsConv.term + let vctxForRhs : VerificationContext := { decl := sourceDecl, stmt := sourceStmt, pathCondition := stateForRhs.pathCondition } + let rhsFailures ← diagnoseConjunct rhs rhsConv stateForRhs vctxForRhs + diagnosements := diagnosements ++ rhsFailures + | _ => pure () + + return { originalCheck := originalResult, diagnosedFailures := diagnosements } + +/-- Diagnose a failed check/assert -/ +def diagnoseFailure (state : B3VerificationState) (expr : B3AST.Expression SourceRange) (sourceDecl : B3AST.Decl SourceRange) (sourceStmt : B3AST.Statement SourceRange) : IO DiagnosisResult := + diagnoseFailureGeneric false state expr sourceDecl sourceStmt + +/-- Diagnose an unreachable reach -/ +def diagnoseUnreachable (state : B3VerificationState) (expr : B3AST.Expression SourceRange) (sourceDecl : B3AST.Decl SourceRange) (sourceStmt : B3AST.Statement SourceRange) : IO DiagnosisResult := + diagnoseFailureGeneric true state expr sourceDecl sourceStmt + +/-- Determine which diagnosis function to use based on statement type -/ +def diagnoseFailed (state : B3VerificationState) (sourceDecl : B3AST.Decl SourceRange) (stmt : B3AST.Statement SourceRange) : IO (Option DiagnosisResult) := + match stmt with + | .check m expr => do + let d ← diagnoseFailure state expr sourceDecl (.check m expr) + pure (some d) + | .assert m expr => do + let d ← diagnoseFailure state expr sourceDecl (.assert m expr) + pure (some d) + | .reach m expr => do + let d ← diagnoseUnreachable state expr sourceDecl (.reach m expr) + pure (some d) + | _ => pure none + +--------------------------------------------------------------------- +-- Statement Symbolic Execution with Diagnosis +--------------------------------------------------------------------- + +/-- Translate statements to SMT with automatic diagnosis on failures (default, recommended). + +This adds diagnosis for failed checks/asserts/reach to help identify root causes. +The diagnosis analyzes failures but does not modify the verification state. + +For faster verification without diagnosis, use statementToSMTWithoutDiagnosis. +-/ +partial def statementToSMT (ctx : ConversionContext) (state : B3VerificationState) (sourceDecl : B3AST.Decl SourceRange) : B3AST.Statement SourceRange → IO SymbolicExecutionResult + | stmt => do + -- Translate the statement to SMT and get results + let execResult ← statementToSMTWithoutDiagnosis ctx state sourceDecl stmt + + -- Add diagnosis to any failed verification results + let mut resultsWithDiagRev := [] + for (stmtResult, _) in execResult.results do + match stmtResult with + | .verified report => + -- If verification failed, diagnose it + let diag ← if report.result.isError then + diagnoseFailed state sourceDecl report.context.stmt + else + pure none + resultsWithDiagRev := (stmtResult, diag) :: resultsWithDiagRev + | .conversionError _ => + -- Conversion errors don't have diagnosis + resultsWithDiagRev := (stmtResult, none) :: resultsWithDiagRev + + pure { results := resultsWithDiagRev.reverse, finalState := execResult.finalState } + +end Strata.B3.Verifier diff --git a/Strata/Languages/B3/Verifier/Expression.lean b/Strata/Languages/B3/Verifier/Expression.lean new file mode 100644 index 00000000..06316dd5 --- /dev/null +++ b/Strata/Languages/B3/Verifier/Expression.lean @@ -0,0 +1,338 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Languages.B3.DDMTransform.DefinitionAST +import Strata.DL.SMT.SMT +import Strata.DL.SMT.Factory +import Strata.Languages.B3.DDMTransform.Conversion + +/-! +# B3 AST to SMT Term Conversion + +Converts B3 abstract syntax trees to SMT terms for verification. +-/ + +namespace Strata.B3.Verifier + +open Strata +open Strata.B3AST +open Strata.SMT +open Strata.SMT.Factory + +--------------------------------------------------------------------- +-- Type Conversion +--------------------------------------------------------------------- + +/-- Convert B3 type name to SMT-LIB type name -/ +def b3TypeToSMT (typeName : String) : String := + match typeName with + | "int" => "Int" + | "bool" => "Bool" + | "real" => "Real" + | "string" => "String" + | other => other -- User-defined types pass through as-is + +--------------------------------------------------------------------- +-- Conversion Context +--------------------------------------------------------------------- + +/-- Errors that can occur during B3 to SMT conversion -/ +inductive ConversionError (M : Type) where + | unsupportedConstruct : String → M → ConversionError M + | unboundVariable : Nat → M → ConversionError M + | typeMismatch : String → M → ConversionError M + | invalidFunctionCall : String → M → ConversionError M + | invalidPattern : String → M → ConversionError M + deriving Inhabited + +namespace ConversionError + +def toString [Repr M] : ConversionError M → String + | unsupportedConstruct msg m => s!"Unsupported construct at {repr m}: {msg}" + | unboundVariable idx m => s!"Unbound variable at index {idx} at {repr m}" + | typeMismatch msg m => s!"Type mismatch at {repr m}: {msg}" + | invalidFunctionCall msg m => s!"Invalid function call at {repr m}: {msg}" + | invalidPattern msg m => s!"Invalid pattern at {repr m}: {msg}" + +instance [Repr M] : ToString (ConversionError M) where + toString := ConversionError.toString + +end ConversionError + +--------------------------------------------------------------------- +-- Conversion Result with Error Accumulation +--------------------------------------------------------------------- + +/-- Conversion result that can carry both a term and errors -/ +structure ConversionResult (M : Type) where + term : Term + errors : List (ConversionError M) + +namespace ConversionResult + +/-- Create a successful conversion result -/ +def ok {M : Type} (term : Term) : ConversionResult M := + { term := term, errors := [] } + +/-- Create a conversion result with an error and placeholder term -/ +def withError {M : Type} (err : ConversionError M) : ConversionResult M := + { term := Term.bool false, errors := [err] } + +end ConversionResult + +structure ConversionContext where + vars : List String -- Maps de Bruijn index to variable name + enableDiagnosis : Bool := true -- Whether to perform automatic diagnosis on failures + +namespace ConversionContext + +def empty : ConversionContext := { vars := [], enableDiagnosis := true } + +def withoutDiagnosis (ctx : ConversionContext) : ConversionContext := + { ctx with enableDiagnosis := false } + +def push (ctx : ConversionContext) (name : String) : ConversionContext := + { ctx with vars := name :: ctx.vars } + +def lookup (ctx : ConversionContext) (idx : Nat) : Option String := + ctx.vars[idx]? + +end ConversionContext + +--------------------------------------------------------------------- +-- Operator Conversion +--------------------------------------------------------------------- + +/-- Placeholder name for UF argument types in SMT encoding. +SMT solvers don't require actual parameter names for uninterpreted functions, +only the types matter for type checking. -/ +def UF_ARG_PLACEHOLDER := "_" + +/-- Convert B3 binary operators to SMT terms without constant folding -/ +def binaryOpToSMT : B3AST.BinaryOp M → (Term → Term → Term) + | .iff _ => fun t1 t2 => Term.app .eq [t1, t2] .bool + | .implies _ => fun t1 t2 => Term.app .implies [t1, t2] .bool + | .impliedBy _ => fun t1 t2 => Term.app .implies [t2, t1] .bool + | .and _ => fun t1 t2 => Term.app .and [t1, t2] .bool + | .or _ => fun t1 t2 => Term.app .or [t1, t2] .bool + | .eq _ => fun t1 t2 => Term.app .eq [t1, t2] .bool + | .neq _ => fun t1 t2 => Term.app .not [Term.app .eq [t1, t2] .bool] .bool + | .lt _ => fun t1 t2 => Term.app .lt [t1, t2] .bool + | .le _ => fun t1 t2 => Term.app .le [t1, t2] .bool + | .ge _ => fun t1 t2 => Term.app .ge [t1, t2] .bool + | .gt _ => fun t1 t2 => Term.app .gt [t1, t2] .bool + | .add _ => fun t1 t2 => Term.app .add [t1, t2] .int + | .sub _ => fun t1 t2 => Term.app .sub [t1, t2] .int + | .mul _ => fun t1 t2 => Term.app .mul [t1, t2] .int + | .div _ => fun t1 t2 => Term.app .div [t1, t2] .int + | .mod _ => fun t1 t2 => Term.app .mod [t1, t2] .int + +/-- Convert B3 unary operators to SMT terms -/ +def unaryOpToSMT : B3AST.UnaryOp M → (Term → Term) + | .not _ => fun t => Term.app .not [t] .bool + | .neg _ => fun t => Term.app .neg [t] .int + +/-- Convert B3 literals to SMT terms -/ +def literalToSMT : B3AST.Literal M → Term + | .intLit _ n => Term.int n + | .boolLit _ b => Term.bool b + | .stringLit _ s => Term.string s + +--------------------------------------------------------------------- +-- Pattern Validation +--------------------------------------------------------------------- + +/-- Collect bound variable indices from a pattern expression. +Returns error if the expression is not structurally valid as a pattern. +Valid patterns consist only of function applications, bound variables, and literals. -/ +def collectPatternBoundVars (expr : B3AST.Expression M) (exprM : M) : Except (ConversionError M) (List Nat) := + match expr with + | .id _ idx => .ok [idx] + | .literal _ _ => .ok [] + | .functionCall _ _ args => do + let results ← args.val.toList.mapM (fun arg => collectPatternBoundVars arg exprM) + return results.flatten + | _ => .error (ConversionError.invalidPattern "patterns must consist only of function applications, variables, and literals" exprM) + termination_by SizeOf.sizeOf expr + decreasing_by + simp_wf + cases args + simp_all + rename_i h + have := Array.sizeOf_lt_of_mem h + omega + +/-- Validate pattern expressions for a quantifier -/ +def validatePatternExprs (patterns : Array (B3AST.Expression M)) (patternM : M) : Except (ConversionError M) Unit := + if patterns.isEmpty then + .ok () -- Empty patterns are OK (solver will auto-generate) + else do + -- Check that each pattern expression is a function application (not just a variable or literal) + for p in patterns do + match p with + | .functionCall _ _ _ => pure () -- Valid + | _ => throw (ConversionError.invalidPattern "each pattern expression must be a function application" patternM) + + -- Collect all bound variables from all patterns + let allBoundVars ← patterns.toList.mapM (fun p => collectPatternBoundVars p patternM) + let flatVars := allBoundVars.flatten + -- Check if the bound variable (id 0) appears in at least one pattern + if !flatVars.contains 0 then + .error (ConversionError.invalidPattern "bound variable must appear in at least one pattern" patternM) + else + .ok () + +--------------------------------------------------------------------- +-- Metadata Extraction +--------------------------------------------------------------------- + +/-- Extract metadata from any B3 expression -/ +def getExpressionMetadata : B3AST.Expression M → M + | .binaryOp m _ _ _ => m + | .literal m _ => m + | .id m _ => m + | .ite m _ _ _ => m + | .unaryOp m _ _ => m + | .functionCall m _ _ => m + | .labeledExpr m _ _ => m + | .letExpr m _ _ _ => m + | .quantifierExpr m _ _ _ _ => m + +--------------------------------------------------------------------- +-- Expression Conversion +--------------------------------------------------------------------- + +/-- Convert B3 expressions to SMT terms with error accumulation -/ +def expressionToSMT (ctx : ConversionContext) (e : B3AST.Expression M) : ConversionResult M := + match e with + | .literal _m lit => + ConversionResult.ok (literalToSMT lit) + + | .id m idx => + match ctx.lookup idx with + | some name => ConversionResult.ok (Term.var ⟨name, .int⟩) + | none => ConversionResult.withError (ConversionError.unboundVariable idx m) + + | .ite _m cond thn els => + let condResult := expressionToSMT ctx cond + let thnResult := expressionToSMT ctx thn + let elsResult := expressionToSMT ctx els + let errors := condResult.errors ++ thnResult.errors ++ elsResult.errors + let term := Term.app .ite [condResult.term, thnResult.term, elsResult.term] thnResult.term.typeOf + { term := term, errors := errors } + + | .binaryOp _m op lhs rhs => + let lhsResult := expressionToSMT ctx lhs + let rhsResult := expressionToSMT ctx rhs + let errors := lhsResult.errors ++ rhsResult.errors + let term := (binaryOpToSMT op) lhsResult.term rhsResult.term + { term := term, errors := errors } + + | .unaryOp _m op arg => + let argResult := expressionToSMT ctx arg + let term := (unaryOpToSMT op) argResult.term + { term := term, errors := argResult.errors } + + | .functionCall m fnName args => + let argResults := args.val.map (fun arg => match _: arg with | a => expressionToSMT ctx a) + let errors := argResults.toList.foldl (fun acc r => acc ++ r.errors) [] + let argTerms := argResults.toList.map (·.term) + let uf : UF := { + id := fnName.val, + args := argTerms.map (fun t => ⟨UF_ARG_PLACEHOLDER, t.typeOf⟩), + out := .int + } + let term := Term.app (.uf uf) argTerms .int + { term := term, errors := errors } + + | .labeledExpr _m _ expr => + expressionToSMT ctx expr + + | .letExpr _m _var value body => + let ctx' := ctx.push _var.val + let valueResult := expressionToSMT ctx value + let bodyResult := expressionToSMT ctx' body + let errors := valueResult.errors ++ bodyResult.errors + { term := bodyResult.term, errors := errors } + + | .quantifierExpr m qkind vars patterns body => + -- Handle multiple quantified variables + let varList := vars.val.toList.filterMap (fun v => + match _: v with + | .quantVarDecl _ name ty => some (name.val, ty.val) + ) + + -- Extend context with all variables + let ctx' := varList.foldl (fun c (name, _) => c.push name) ctx + + -- Convert body + let bodyResult := expressionToSMT ctx' body + + -- Convert pattern expressions and collect errors + let patternResults : Array (List Term × List (ConversionError M)) := patterns.val.map (fun p => + match _: p with + | .pattern _ exprs => + let results : Array (ConversionResult M) := exprs.val.map (fun e => match _: e with | expr => expressionToSMT ctx' expr) + (results.toList.map (·.term), results.toList.foldl (fun acc r => acc ++ r.errors) []) + ) + let patternTermLists : List (List Term) := patternResults.toList.map (·.1) + let patternErrors : List (ConversionError M) := patternResults.toList.foldl (fun acc r => acc ++ r.2) [] + + -- Validate pattern structure + let patternExprArray := patterns.val.flatMap (fun p => + match _: p with + | .pattern _ exprs => exprs.val + ) + let validationErrors := match validatePatternExprs patternExprArray m with + | .ok () => [] + | .error err => [err] + + -- Build trigger from pattern terms + let allPatternTerms := patternTermLists.foldl (· ++ ·) [] + let trigger := if patterns.val.isEmpty then + -- No patterns specified in source - don't generate a trigger + Term.app .triggers [] .trigger + else if allPatternTerms.isEmpty then + -- Patterns specified but empty (shouldn't happen) - generate simple trigger for first var + match varList.head? with + | some (name, _) => Factory.mkSimpleTrigger name .int + | none => Term.app .triggers [] .trigger + else + -- Patterns specified - use them + allPatternTerms.foldl (fun acc term => Factory.addTrigger term acc) (Term.app .triggers [] .trigger) + + -- Build quantifier term with all variables + let qk := match _: qkind with + | .forall _ => QuantifierKind.all + | .exists _ => QuantifierKind.exist + + let term := varList.foldr (fun (name, _ty) body => + Factory.quant qk name .int trigger body + ) bodyResult.term + + -- Accumulate all errors + let allErrors := bodyResult.errors ++ validationErrors ++ patternErrors + { term := term, errors := allErrors } + + termination_by SizeOf.sizeOf e + decreasing_by + all_goals (simp_wf <;> try omega) + . cases args; simp_all + rename_i h; have := Array.sizeOf_lt_of_mem h; omega + . cases exprs; cases patterns; simp_all; subst_vars + rename_i h1 h2 + have := Array.sizeOf_lt_of_mem h1 + have Hpsz := Array.sizeOf_lt_of_mem h2 + simp at Hpsz; omega + +def formatExpression (prog : Program) (expr : B3AST.Expression SourceRange) (ctx: B3.ToCSTContext): String := + let (cstExpr, _) := B3.expressionToCST ctx expr + let ctx := FormatContext.ofDialects prog.dialects prog.globalContext {} + let fmtState : FormatState := { openDialects := prog.dialects.toList.foldl (init := {}) fun a (dialect : Dialect) => a.insert dialect.name } + let formatted := (mformat (ArgF.op cstExpr.toAst) ctx fmtState).format.pretty.trim + formatted + +end Strata.B3.Verifier diff --git a/Strata/Languages/B3/Verifier/Formatter.lean b/Strata/Languages/B3/Verifier/Formatter.lean new file mode 100644 index 00000000..a7bcb9f7 --- /dev/null +++ b/Strata/Languages/B3/Verifier/Formatter.lean @@ -0,0 +1,28 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.DL.SMT.DDMTransform.Translate + +/-! +# SMT Term Formatting + +Formats SMT terms to SMT-LIB syntax using the SMT dialect's pretty-printer. + +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. +-/ + +namespace Strata.B3.Verifier + +open Strata.SMT + +/-- Format SMT term to SMT-LIB syntax using the SMT dialect's pretty-printer -/ +def formatTermDirect (t : Term) : String := + match SMTDDM.toString t with + | .ok s => s + | .error msg => s!"(error: {msg})" + +end Strata.B3.Verifier diff --git a/Strata/Languages/B3/Verifier/Program.lean b/Strata/Languages/B3/Verifier/Program.lean new file mode 100644 index 00000000..878a3188 --- /dev/null +++ b/Strata/Languages/B3/Verifier/Program.lean @@ -0,0 +1,202 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Languages.B3.Verifier.State +import Strata.Languages.B3.Verifier.Expression +import Strata.Languages.B3.Verifier.Formatter +import Strata.Languages.B3.Verifier.Statements +import Strata.Languages.B3.Verifier.Diagnosis +import Strata.Languages.B3.Transform.FunctionToAxiom +import Strata.Languages.B3.DDMTransform.Conversion + +/-! +# B3 Program Verification + +Program-level verification API for B3 programs. +Verifies entire programs with automatic diagnosis. +-/ + +namespace Strata.B3.Verifier + +open Strata +open Strata.SMT +open Strata.B3AST + +--------------------------------------------------------------------- +-- Batch Verification API +--------------------------------------------------------------------- + +/-- Extract function declarations from a B3 program -/ +def extractFunctionDeclarations (prog : B3AST.Program SourceRange) : List (String × List String × String) := + match prog with + | .program _ decls => + decls.val.toList.filterMap (fun decl => + match decl with + | .function _ name params resultType _ body => + if body.val.isNone then + let argTypes := params.val.toList.map (fun p => + match p with + | .fParameter _ _ _ ty => b3TypeToSMT ty.val + ) + let retType := b3TypeToSMT resultType.val + some (name.val, argTypes, retType) + else + none + | _ => none + ) + +/-- Extract axiom expressions from a B3 program -/ +def extractAxioms (prog : B3AST.Program SourceRange) : List (B3AST.Expression SourceRange) := + match prog with + | .program _ decls => + decls.val.toList.filterMap (fun decl => + match decl with + | .axiom _ _ expr => some expr + | _ => none + ) + +/-- Add declarations and axioms from a transformed B3 program to the verification state -/ +private def addDeclarationsAndAxioms (state : B3VerificationState) (prog : B3AST.Program SourceRange) : IO (B3VerificationState × List String) := do + let mut state := state + let mut errors := [] + + -- Add function declarations + for (name, argTypes, retType) in extractFunctionDeclarations prog do + state ← addFunctionDecl state name argTypes retType + + -- Add axioms + for expr in extractAxioms prog do + let convResult := expressionToSMT ConversionContext.empty expr + state ← addPathCondition state expr convResult.term + errors := errors ++ convResult.errors.map toString + + return (state, errors) + +/-- Extract parameter-free procedures with bodies from a B3 program -/ +def extractVerifiableProcedures (prog : B3AST.Program SourceRange) : List (String × B3AST.Decl SourceRange × B3AST.Statement SourceRange) := + match prog with + | .program _ decls => + decls.val.toList.filterMap (fun decl => + match decl with + | .procedure _ name params _ body => + if params.val.isEmpty && body.val.isSome then + some (name.val, decl, body.val.get!) + else + none + | _ => none + ) + +/-- Translate a B3 program to SMT without automatic diagnosis (faster, less detailed errors) -/ +def programToSMTWithoutDiagnosis (prog : B3AST.Program SourceRange) (solver : Solver) : IO (List (Except String VerificationReport)) := do + let initialState ← initVerificationState solver + let mut results := [] + + -- Transform: split functions into declarations + axioms + let transformedProg := Transform.functionToAxiom prog + + -- Add function declarations and axioms + let (state, conversionErrors) ← addDeclarationsAndAxioms initialState transformedProg + + -- Report conversion errors + results := results ++ conversionErrors.map .error + + -- Verify parameter-free procedures + for (_name, decl, bodyStmt) in extractVerifiableProcedures prog do + let execResult ← statementToSMTWithoutDiagnosis ConversionContext.empty state decl bodyStmt + -- Extract just the StatementResults (no diagnosis) + let stmtResults := execResult.results.map (·.1) + results := results ++ stmtResults.map StatementResult.toExcept + + closeVerificationState state + return results + +--------------------------------------------------------------------- +-- Convenience Wrappers +--------------------------------------------------------------------- + +/-- Convert DDM Program to B3 AST with error handling -/ +def programToB3AST (prog : Program) : Except String (B3AST.Program SourceRange) := do + let [op] ← pure prog.commands.toList + | .error "Expected single program command" + + if op.name.name != "command_program" then + .error s!"Expected command_program, got {op.name.name}" + + let [ArgF.op progOp] ← pure op.args.toList + | .error "Expected single program argument" + + let cstProg ← B3CST.Program.ofAst progOp + + let (ast, errors) := B3.programFromCST B3.FromCSTContext.empty cstProg + if !errors.isEmpty then + .error s!"CST to AST conversion errors: {errors}" + else + .ok ast + +/-- Build verification state from B3 program (functions and axioms only, no procedures) -/ +def buildProgramState (prog : Strata.B3AST.Program SourceRange) (solver : Solver) : IO B3VerificationState := do + let state ← initVerificationState solver + let transformedProg := Transform.functionToAxiom prog + let (newState, errors) ← addDeclarationsAndAxioms state transformedProg + -- Log errors if any + for err in errors do + IO.eprintln s!"Warning: {err}" + return newState + +/-- Generate SMT commands for a B3 program -/ +def programToSMTCommands (prog : Strata.B3AST.Program SourceRange) : IO String := do + let (solver, buffer) ← createBufferSolver + let _ ← (Solver.setLogic "ALL").run solver + let _ ← programToSMTWithoutDiagnosis prog solver + let contents ← buffer.get + if h: contents.data.IsValidUTF8 + then return String.fromUTF8 contents.data h + else return "Error: Invalid UTF-8 in SMT output" + +--------------------------------------------------------------------- +-- Batch Verification with Automatic Diagnosis +--------------------------------------------------------------------- + +structure ProcedureReport where + procedureName : String + results : List (VerificationReport × Option DiagnosisResult) + +/-- Translate a B3 program to SMT and verify with automatic diagnosis. + +Main entry point for verification. + +Workflow: +1. Build program state (functions, axioms) +2. For each parameter-free procedure: + - Translate statements to SMT + - Check each VC + - If failed, automatically diagnose to find root cause +3. Report all results with diagnosis + +The solver is reset at the beginning to ensure clean state. +-/ +def programToSMT (prog : Strata.B3AST.Program SourceRange) (solver : Solver) : IO (List ProcedureReport) := do + -- Reset solver to clean state + let _ ← (Solver.reset).run solver + let state ← buildProgramState prog solver + let mut reportsRev := [] + + -- Verify parameter-free procedures + for (name, decl, bodyStmt) in extractVerifiableProcedures prog do + let execResult ← statementToSMT ConversionContext.empty state decl bodyStmt + -- Extract VerificationReports with diagnosis + let resultsWithDiag := execResult.results.filterMap (fun (stmtResult, diag) => + match stmtResult with + | .verified report => some (report, diag) + | .conversionError _ => none + ) + reportsRev := { + procedureName := name + results := resultsWithDiag + } :: reportsRev + + closeVerificationState state + return reportsRev.reverse diff --git a/Strata/Languages/B3/Verifier/State.lean b/Strata/Languages/B3/Verifier/State.lean new file mode 100644 index 00000000..caedc231 --- /dev/null +++ b/Strata/Languages/B3/Verifier/State.lean @@ -0,0 +1,201 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Languages.B3.Verifier.Expression +import Strata.Languages.B3.Verifier.Formatter +import Strata.Languages.B3.DDMTransform.DefinitionAST +import Strata.DL.SMT.Solver + +/-! +# B3 Verification State + +Manages incremental verification state for interactive debugging. +-/ + +namespace Strata.B3.Verifier + +open Strata +open Strata.SMT +open Strata.B3AST +open Strata.B3.Verifier (UF_ARG_PLACEHOLDER) + +--------------------------------------------------------------------- +-- B3 Verification Results +--------------------------------------------------------------------- + +/-- Verification outcome when check fails -/ +inductive VerificationError where + | counterexample : VerificationError -- Possibly wrong (sat) + | unknown : VerificationError -- Couldn't determine + | refuted : VerificationError -- Proved false/unreachable (unsat) + +/-- Verification outcome when check succeeds -/ +inductive VerificationSuccess where + | verified : VerificationSuccess -- Proved + | reachable : VerificationSuccess -- Reachability confirmed + | reachabilityUnknown : VerificationSuccess -- Couldn't determine, but not an error + +/-- Unified verification result -/ +inductive VerificationResult where + | error : VerificationError → VerificationResult + | success : VerificationSuccess → VerificationResult + +def VerificationResult.isError : VerificationResult → Bool + | .error _ => true + | .success _ => false + +def VerificationResult.fromDecisionForProve (d : Decision) : VerificationResult := + match d with + | .unsat => .success .verified + | .sat => .error .counterexample + | .unknown => .error .unknown + +def VerificationResult.fromDecisionForReach (d : Decision) : VerificationResult := + match d with + | .unsat => .error .refuted + | .sat => .success .reachable + | .unknown => .success .reachabilityUnknown + +--------------------------------------------------------------------- +-- Verification Context and Results +--------------------------------------------------------------------- + +/-- Context for a verification check (where in the program and what we know) -/ +structure VerificationContext where + decl : B3AST.Decl SourceRange + stmt : B3AST.Statement SourceRange + pathCondition : List (B3AST.Expression SourceRange) -- Accumulated assertions + +/-- VerificationReport combines VerificationResult with source context. +Top-level result type returned to users, containing: +- The verification result (proved/counterexample/reachable/etc.) +- Source context (declaration, statement, and path condition) +- Optional model/counterexample information (TODO: use structured Model type instead of String) +-/ +structure VerificationReport where + context : VerificationContext + result : VerificationResult + model : Option String := none -- TODO: Replace with structured Model type (Map String Term) + +--------------------------------------------------------------------- +-- SMT Solver State +--------------------------------------------------------------------- + +/-- SMT solver state (reusable for any language) -/ +structure SMTSolverState where + solver : Solver + declaredFunctions : List (String × List String × String) + assertions : List Term + +/-- B3-specific verification state -/ +structure B3VerificationState where + smtState : SMTSolverState + context : ConversionContext + pathCondition : List (B3AST.Expression SourceRange) -- Accumulated assertions for debugging + +def initVerificationState (solver : Solver) : IO B3VerificationState := do + let _ ← (Solver.setLogic "ALL").run solver + let _ ← (Solver.setOption "produce-models" "true").run solver + return { + smtState := { + solver := solver + declaredFunctions := [] + assertions := [] + } + context := ConversionContext.empty + pathCondition := [] + } + +def addFunctionDecl (state : B3VerificationState) (name : String) (argTypes : List String) (returnType : String) : IO B3VerificationState := do + let _ ← (Solver.declareFun name argTypes returnType).run state.smtState.solver + return { state with smtState := { state.smtState with declaredFunctions := (name, argTypes, returnType) :: state.smtState.declaredFunctions } } + +def addPathCondition (state : B3VerificationState) (expr : B3AST.Expression SourceRange) (term : Term) : IO B3VerificationState := do + let _ ← (Solver.assert (formatTermDirect term)).run state.smtState.solver + return { + state with + smtState := { state.smtState with assertions := term :: state.smtState.assertions } + pathCondition := expr :: state.pathCondition + } + +def push (state : B3VerificationState) : IO B3VerificationState := do + let solver := state.smtState.solver + solver.smtLibInput.putStr "(push 1)\n" + solver.smtLibInput.flush + return state + +def pop (state : B3VerificationState) : IO B3VerificationState := do + let solver := state.smtState.solver + solver.smtLibInput.putStr "(pop 1)\n" + solver.smtLibInput.flush + return state + +/-- Prove a property holds (check/assert statement) -/ +def prove (state : B3VerificationState) (term : Term) (ctx : VerificationContext) : IO VerificationReport := do + let _ ← push state + let runCheck : SolverM (Decision × Option String) := do + Solver.assert s!"(not {formatTermDirect term})" + let decision ← Solver.checkSat [] + let model := if decision == .sat then some "model available" else none + return (decision, model) + let (decision, model) ← runCheck.run state.smtState.solver + let _ ← pop state + return { + context := ctx + result := VerificationResult.fromDecisionForProve decision + model := model + } + +/-- Check if a property is reachable (reach statement) -/ +def reach (state : B3VerificationState) (term : Term) (ctx : VerificationContext) : IO VerificationReport := do + let _ ← push state + let runCheck : SolverM (Decision × Option String) := do + Solver.assert (formatTermDirect term) + let decision ← Solver.checkSat [] + let model := if decision == .sat then some "reachable" else none + return (decision, model) + let (decision, model) ← runCheck.run state.smtState.solver + let _ ← pop state + return { + context := ctx + result := VerificationResult.fromDecisionForReach decision + model := model + } + +def closeVerificationState (state : B3VerificationState) : IO Unit := do + let _ ← (Solver.exit).run state.smtState.solver + pure () + +--------------------------------------------------------------------- +-- Solver Creation Helpers +--------------------------------------------------------------------- + +/-- Create an interactive solver (Z3/CVC5) -/ +def createInteractiveSolver (solverPath : String := "z3") : IO Solver := + let args := if solverPath.endsWith "cvc5" || solverPath == "cvc5" + then #["--lang", "smt2", "--incremental"] + else #["-smt2", "-in"] -- Z3 flags + Solver.spawn solverPath args + +/-- Create a buffer solver for SMT command generation -/ +def createBufferSolver : IO (Solver × IO.Ref IO.FS.Stream.Buffer) := do + let buffer ← IO.mkRef {} + let solver ← Solver.bufferWriter buffer + return (solver, buffer) + +--------------------------------------------------------------------- +-- Verification Results +--------------------------------------------------------------------- + +structure DiagnosedFailure where + expression : B3AST.Expression SourceRange + report : VerificationReport -- Contains context (with pathCondition), result (refuted if provably false), model + +structure DiagnosisResult where + originalCheck : VerificationReport + diagnosedFailures : List DiagnosedFailure + +end Strata.B3.Verifier diff --git a/Strata/Languages/B3/Verifier/Statements.lean b/Strata/Languages/B3/Verifier/Statements.lean new file mode 100644 index 00000000..d8ec12fd --- /dev/null +++ b/Strata/Languages/B3/Verifier/Statements.lean @@ -0,0 +1,114 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Languages.B3.Verifier.Expression +import Strata.Languages.B3.Verifier.State +import Strata.Languages.B3.DDMTransform.ParseCST +import Strata.Languages.B3.DDMTransform.Conversion +import Strata.DDM.Integration.Lean +import Strata.DDM.Util.Format + +/-! +# B3 Statement Streaming Translation + +Translates B3 statements to SMT via streaming symbolic execution (NOT batch VCG). + +## Streaming Symbolic Execution + +Statements are translated and symbolically executed immediately: +- `assert e` - prove e, then add to solver state (assumes e regardless of proof result) +- `check e` - prove e (push/pop, doesn't affect state) +- `assume e` - add to solver state +- `reach e` - check satisfiability (push/pop) + +This allows the solver to learn from asserts, making later checks easier. +Key advantage: O(n) not O(n²), solver accumulates lemmas. +-/ + +namespace Strata.B3.Verifier + +open Strata +open Strata.SMT + +inductive StatementResult where + | verified : VerificationReport → StatementResult + | conversionError : String → StatementResult + +/-- Convert StatementResult to Except for easier error handling -/ +def StatementResult.toExcept : StatementResult → Except String VerificationReport + | .verified report => .ok report + | .conversionError msg => .error msg + +structure SymbolicExecutionResult where + results : List (StatementResult × Option DiagnosisResult) + finalState : B3VerificationState + +/-- Convert conversion errors to StatementResults -/ +def conversionErrorsToResults {M : Type} [Repr M] (errors : List (ConversionError M)) : List StatementResult := + errors.map (fun err => StatementResult.conversionError (toString err)) + +/-- Create VerificationContext from state and statement -/ +def mkVerificationContext (state : B3VerificationState) (decl : B3AST.Decl SourceRange) (stmt : B3AST.Statement SourceRange) : VerificationContext := + { decl := decl, stmt := stmt, pathCondition := state.pathCondition } + +/-- Create a SymbolicExecutionResult with conversion errors and optional verification result -/ +def mkExecutionResult {M : Type} [Repr M] (convErrors : List (ConversionError M)) (verificationResult : Option VerificationReport) (state : B3VerificationState) : SymbolicExecutionResult := + let errorResults := conversionErrorsToResults convErrors + let allResults := match verificationResult with + | some report => errorResults.map (·, none) ++ [(StatementResult.verified report, none)] + | none => errorResults.map (·, none) + { results := allResults, finalState := state } + +/-- Translate B3 statements to SMT via streaming symbolic execution (without diagnosis) -/ +partial def statementToSMTWithoutDiagnosis (ctx : ConversionContext) (state : B3VerificationState) (sourceDecl : B3AST.Decl SourceRange) : B3AST.Statement SourceRange → IO SymbolicExecutionResult + | .check m expr => do + let convResult := expressionToSMT ctx expr + let vctx := mkVerificationContext state sourceDecl (.check m expr) + let result ← prove state convResult.term vctx + pure <| mkExecutionResult convResult.errors (some result) state + + | .assert m expr => do + let convResult := expressionToSMT ctx expr + let vctx := mkVerificationContext state sourceDecl (.assert m expr) + let result ← prove state convResult.term vctx + -- Always add to path condition (assert assumes its condition regardless of proof result) + let newState ← addPathCondition state expr convResult.term + pure <| mkExecutionResult convResult.errors (some result) newState + + | .assume _ expr => do + let convResult := expressionToSMT ctx expr + let newState ← addPathCondition state expr convResult.term + pure <| mkExecutionResult convResult.errors none newState + + | .reach m expr => do + let convResult := expressionToSMT ctx expr + let vctx := mkVerificationContext state sourceDecl (.reach m expr) + let result ← reach state convResult.term vctx + pure <| mkExecutionResult convResult.errors (some result) state + + | .blockStmt _ stmts => do + let mut currentState := state + let mut allResultsRev := [] + for stmt in stmts.val.toList do + let execResult ← statementToSMTWithoutDiagnosis ctx currentState sourceDecl stmt + currentState := execResult.finalState + allResultsRev := execResult.results.reverse ++ allResultsRev + pure { results := allResultsRev.reverse, finalState := currentState } + + | _ => + pure { results := [], finalState := state } + +--------------------------------------------------------------------- +-- Statement Formatting +--------------------------------------------------------------------- + +def formatStatement (prog : Program) (stmt : B3AST.Statement SourceRange) (ctx: B3.ToCSTContext): String := + let (cstStmt, _) := B3.stmtToCST ctx stmt + let fmtCtx := FormatContext.ofDialects prog.dialects prog.globalContext {} + let fmtState : FormatState := { openDialects := prog.dialects.toList.foldl (init := {}) fun a (dialect : Dialect) => a.insert dialect.name } + (mformat (ArgF.op cstStmt.toAst) fmtCtx fmtState).format.pretty.trim + +end Strata.B3.Verifier diff --git a/StrataTest/Languages/B3/Verifier/TranslationTests.lean b/StrataTest/Languages/B3/Verifier/TranslationTests.lean new file mode 100644 index 00000000..c7fc39c6 --- /dev/null +++ b/StrataTest/Languages/B3/Verifier/TranslationTests.lean @@ -0,0 +1,185 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Languages.B3.Verifier +import Strata.Languages.B3.DDMTransform.ParseCST +import Strata.Languages.B3.DDMTransform.Conversion + +/-! +# B3 to SMT Translation Tests + +Tests for B3 AST to SMT-LIB translation. +These tests verify the generated SMT-LIB output without running solvers. +-/ + +namespace B3.Verifier.TranslationTests + +open Strata +open Strata.B3.Verifier + +--------------------------------------------------------------------- +-- Test Helpers +--------------------------------------------------------------------- + +def testSMTGeneration (prog : Program) : IO Unit := do + let ast ← match programToB3AST prog with + | .ok ast => pure ast + | .error msg => throw (IO.userError s!"Parse error: {msg}") + + -- Create a buffer solver to capture SMT commands + let (solver, buffer) ← createBufferSolver + + -- Run verification to get both SMT and errors + let results ← programToSMTWithoutDiagnosis ast solver + + -- Collect and print conversion errors first (strip location info for stable tests) + let errors := results.filterMap (fun r => + match r with + | .error msg => some msg + | .ok _ => none + ) + for err in errors do + -- Strip location information (anything between "at {" and "}: ") for stable tests + let cleanErr := err.splitOn "at {" |>.head! + let suffix := err.splitOn "}: " |>.tail.headD "" + let finalErr := if suffix.isEmpty then cleanErr else cleanErr ++ suffix + IO.println s!"error: {finalErr.trim}" + + -- Get and print SMT commands + let contents ← buffer.get + let commands := if h: contents.data.IsValidUTF8 + then String.fromUTF8 contents.data h + else "Error: Invalid UTF-8 in SMT output" + + -- Strip common prefix/suffix for stable tests + let lines := commands.splitOn "\n" + let filtered := lines.filter (fun line => + !line.startsWith "(set-logic" && + !line.startsWith "(set-option" && + !line.startsWith "(exit" + ) + IO.println (String.intercalate "\n" filtered) + +--------------------------------------------------------------------- +-- SMT Generation Tests +--------------------------------------------------------------------- + +/-- +info: (declare-fun abs (Int) Int) +(assert (forall ((x Int)) (! (= (abs x) (ite (>= x 0) x (- x))) :pattern ((abs x))))) +(push 1) +(assert (not (= (abs (- 5)) 5))) +(check-sat) +(pop 1) +-/ +#guard_msgs in +#eval testSMTGeneration $ #strata program B3CST; +function abs(x : int) : int { + if x >= 0 x else -x +} +procedure test() { + check abs(-5) == 5 +} +#end + +/-- +info: (declare-fun isEven (Int) Int) +(declare-fun isOdd (Int) Int) +(assert (forall ((n Int)) (! (= (isEven n) (ite (= n 0) 1 (isOdd (- n 1)))) :pattern ((isEven n))))) +(assert (forall ((n Int)) (! (= (isOdd n) (ite (= n 0) 0 (isEven (- n 1)))) :pattern ((isOdd n))))) +(push 1) +(assert (not (= (isEven 4) 1))) +(check-sat) +(pop 1) +-/ +#guard_msgs in +#eval testSMTGeneration $ #strata program B3CST; +function isEven(n : int) : int { + if n == 0 1 else isOdd(n - 1) +} +function isOdd(n : int) : int { + if n == 0 0 else isEven(n - 1) +} +procedure test() { + check isEven(4) == 1 +} +#end + +/-- +info: (declare-fun f (Int) Int) +(assert (forall ((x Int)) (! (=> (> x 0) (> (f x) 0)) :pattern ((f x))))) +(push 1) +(assert (not (=> (> 5 0) (> (f 5) 0)))) +(check-sat) +(pop 1) +-/ +#guard_msgs in +#eval testSMTGeneration $ #strata program B3CST; +function f(x : int) : int +axiom forall x : int pattern f(x) x > 0 ==> f(x) > 0 +procedure test() { + check 5 > 0 ==> f(5) > 0 +} +#end + +/-- +info: (declare-fun f (Int) Bool) +(declare-fun g (Int Int) Bool) +(assert (forall ((x Int)) (! (= (f x) (= (+ x 1) 6)) :pattern ((f x))))) +(push 1) +(assert (not (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= 5 5) (not (= 3 4))) (< 2 3)) (<= 2 2)) (> 4 3)) (>= 4 4)) (= (+ 1 2) 4)) (= (- 5 2) 3)) (= (* 3 4) 12)) (= (div 10 2) 5)) (= (mod 7 3) 1)) (= (- 5) (- 0 5))) (=> true true)) (or false true)) (ite true true false)) (f 5)) (g 1 2)) (forall ((y Int)) (! (or (f y) (not (f y))) :pattern ((f y))))) (forall ((y Int)) (or (> y 0) (<= y 0)))))) +(check-sat) +(pop 1) +-/ +#guard_msgs in +#eval testSMTGeneration $ #strata program B3CST; +function f(x : int) : bool { x + 1 == 6 } +function g(a : int, b : int) : bool +procedure test_all_expressions() { + check 5 == 5 && + !(3 == 4) && + 2 < 3 && + 2 <= 2 && + 4 > 3 && + 4 >= 4 && + 1 + 2 == 4 && + 5 - 2 == 3 && + 3 * 4 == 12 && + 10 div 2 == 5 && + 7 mod 3 == 1 && + -5 == 0 - 5 && + (true ==> true) && + (false || true) && + (if true true else false) && + f(5) && + g(1, 2) && + (forall y : int pattern f(y) f(y) || !f(y)) && + (forall y : int y > 0 || y <= 0) +} +#end + +--------------------------------------------------------------------- +-- Invalid Pattern Tests +--------------------------------------------------------------------- + +-- The test below should return an error and the SMT code. +/-- +info: error: Invalid pattern each pattern expression must be a function application +(declare-fun f (Int) Bool) +(push 1) +(assert (not (forall ((y Int)) (! (> y 0) :pattern (y))))) +(check-sat) +(pop 1) +-/ +#guard_msgs in +#eval testSMTGeneration $ #strata program B3CST; +function f(x : int) : bool +procedure test_invalid_pattern() { + check forall y : int pattern y y > 0 +} +#end + +end B3.Verifier.TranslationTests diff --git a/StrataTest/Languages/B3/Verifier/VerifierTests.lean b/StrataTest/Languages/B3/Verifier/VerifierTests.lean new file mode 100644 index 00000000..1ad405b7 --- /dev/null +++ b/StrataTest/Languages/B3/Verifier/VerifierTests.lean @@ -0,0 +1,544 @@ +/- + Copyright Strata Contributors + + SPDX-License-Identifier: Apache-2.0 OR MIT +-/ + +import Strata.Languages.B3.Verifier +import Strata.Languages.B3.DDMTransform.ParseCST +import Strata.Languages.B3.DDMTransform.Conversion +import Strata.DL.SMT.Solver + +/-! +# B3 Verifier Integration Tests + +Tests for B3 verification with SMT solvers (Z3/CVC5). +These tests run the actual solver and test check, assert, reach statements with automatic diagnosis. + +## Implementation Status + +**Expressions:** +- ✅ Literals (int, bool, string) +- ✅ Binary operators (==, !=, <, <=, >, >=, +, -, *, div, mod, &&, ||, ==>, <==, <==>) +- ✅ Unary operators (!, -) +- ✅ If-then-else +- ✅ Function calls +- ✅ Quantifiers (forall, exists) with patterns +- ✅ Labeled expressions (labels stripped) +- ❌ Let expressions (needs proper substitution) + +**Declarations:** +- ✅ Function declarations +- ✅ Function bodies → quantified axioms +- ✅ Axioms +- ❌ Explains clauses (parsed but ignored) +- ❌ Type declarations +- ❌ Tagger declarations +- ❌ Injective parameters → inverse functions +- ❌ Tagged functions → tag constants +- ❌ When clauses (parsed but not fully tested) + +**Statements:** +- ✅ Check (verify property) +- ✅ Assert (verify and assume) +- ✅ Assume (add to solver) +- ✅ Reach (reachability) +- ✅ Block statements +- ❌ Probe statements +- ❌ Variable declarations (var, val) +- ❌ Assignments +- ❌ Reinit +- ❌ If statements +- ❌ If-case statements +- ❌ Choose statements +- ❌ Loop statements with invariants +- ❌ Labeled statements +- ❌ Exit/Return statements +- ❌ Forall statements (aForall) + +**Procedures:** +- ✅ Parameter-free procedures +- ❌ Procedures with parameters (in, out, inout) + +**Error Handling:** +- ✅ Error accumulation (conversion errors don't short-circuit) +- ✅ Pattern validation with error reporting +- ✅ Recursive diagnosis of failing conjunctions +- ✅ Context-aware diagnosis (assumes earlier conjuncts when diagnosing later ones) + +-/ + +namespace B3.Verifier.Tests + +open Strata +open Strata.B3.Verifier +open Strata.SMT + +--------------------------------------------------------------------- +-- Test Helpers +--------------------------------------------------------------------- + +-- Diagnostic message constants for consistency +private def MSG_COULD_NOT_PROVE := "could not prove" +private def MSG_IMPOSSIBLE := "it is impossible that" +private def MSG_UNDER_ASSUMPTIONS := "under the assumptions" + +def formatSourceLocation (baseOffset : String.Pos.Raw) (sr : SourceRange) : String := + let relativePos := sr.start.byteIdx - baseOffset.byteIdx + s!"(0,{relativePos})" + +def formatStatementError (prog : Program) (stmt : B3AST.Statement SourceRange) : String := + let baseOffset := match prog.commands.toList with + | [op] => op.ann.start + | _ => { byteIdx := 0 } + let loc := formatSourceLocation baseOffset stmt.metadata + let formatted := formatStatement prog stmt B3.ToCSTContext.empty + s!"{loc}: {formatted}" + +def formatExpressionError (prog : Program) (expr : B3AST.Expression SourceRange) : String := + let baseOffset := match prog.commands.toList with + | [op] => op.ann.start + | _ => { byteIdx := 0 } + let loc := formatSourceLocation baseOffset (getExpressionMetadata expr) + + let formatted := formatExpression prog expr B3.ToCSTContext.empty + + s!"{loc}: {formatted}" + +def formatExpressionLocation (prog : Program) (expr : B3AST.Expression SourceRange) : String := + let baseOffset := match prog.commands.toList with + | [op] => op.ann.start + | _ => { byteIdx := 0 } + formatSourceLocation baseOffset (getExpressionMetadata expr) + +def formatExpressionOnly (prog : Program) (expr : B3AST.Expression SourceRange) : String := + let (cstExpr, _) := B3.expressionToCST B3.ToCSTContext.empty expr + let ctx := FormatContext.ofDialects prog.dialects prog.globalContext {} + let fmtState : FormatState := { openDialects := prog.dialects.toList.foldl (init := {}) fun a (dialect : Dialect) => a.insert dialect.name } + (mformat (ArgF.op cstExpr.toAst) ctx fmtState).format.pretty.trim + +/-- Flatten conjunctions into a list of conjuncts for display -/ +def flattenConjunction : B3AST.Expression SourceRange → List (B3AST.Expression SourceRange) + | .binaryOp _ (.and _) lhs rhs => flattenConjunction lhs ++ flattenConjunction rhs + | expr => [expr] + termination_by e => SizeOf.sizeOf e + +def testVerification (prog : Program) : IO Unit := do + let result : Except String (B3AST.Program SourceRange) := programToB3AST prog + let ast ← match result with + | .ok ast => pure ast + | .error msg => throw (IO.userError s!"Parse error: {msg}") + -- Create a fresh solver for each test to avoid state issues + let solver ← createInteractiveSolver "cvc5" + let reports ← programToSMT ast solver + -- Don't call exit - let the solver process terminate naturally + for report in reports do + for (result, diagnosis) in report.results do + match result.context.decl with + | .procedure _ name _ _ _ => + let marker := if result.result.isError then "✗" else "✓" + let description := match result.result with + | .error .counterexample => "counterexample found" + | .error .unknown => "unknown" + | .error .refuted => "refuted" + | .success .verified => "verified" + | .success .reachable => "reachable" + | .success .reachabilityUnknown => "reachability unknown" + + IO.println s!"{name.val}: {marker} {description}" + if result.result.isError then + let baseOffset := match prog.commands.toList with + | [op] => op.ann.start + | _ => { byteIdx := 0 } + + let stmt := result.context.stmt + IO.println s!" {formatStatementError prog stmt}" + + -- Display diagnosis with VC for each failure, or top-level VC if no diagnosis + match diagnosis with + | some diag => + if !diag.diagnosedFailures.isEmpty then + -- Show diagnosis with assumptions for each failure + for failure in diag.diagnosedFailures do + let exprLoc := formatExpressionLocation prog failure.expression + let exprFormatted := formatExpressionOnly prog failure.expression + let diagnosisPrefix := match failure.report.result with + | .error .refuted => MSG_IMPOSSIBLE + | .error .counterexample | .error .unknown => MSG_COULD_NOT_PROVE + | .success _ => MSG_COULD_NOT_PROVE -- Shouldn't happen + + -- Get statement location for comparison + let stmtLoc := match stmt with + | .check m _ | .assert m _ | .reach m _ => formatSourceLocation baseOffset m + | _ => "" + + -- Only show location if different from statement location + if exprLoc == stmtLoc then + IO.println s!" └─ {diagnosisPrefix} {exprFormatted}" + else + IO.println s!" └─ {exprLoc}: {diagnosisPrefix} {exprFormatted}" + + -- Show assumptions for this failure (from report context) + if !failure.report.context.pathCondition.isEmpty then + IO.println s!" {MSG_UNDER_ASSUMPTIONS}" + for expr in failure.report.context.pathCondition.reverse do + -- Flatten conjunctions to show each on separate line + for conjunct in flattenConjunction expr do + let formatted := formatExpressionOnly prog conjunct + IO.println s!" {formatted}" + else + -- No specific diagnosis - use same format with └─ + if !result.context.pathCondition.isEmpty then + match stmt with + | .check m expr | .assert m expr => + let exprLoc := formatSourceLocation baseOffset m + let formatted := formatExpressionOnly prog expr + IO.println s!" └─ {exprLoc}: {MSG_COULD_NOT_PROVE} {formatted}" + IO.println s!" {MSG_UNDER_ASSUMPTIONS}" + for expr in result.context.pathCondition.reverse do + -- Flatten conjunctions to show each on separate line + for conjunct in flattenConjunction expr do + let formatted := formatExpressionOnly prog conjunct + IO.println s!" {formatted}" + | .reach m expr => + let exprLoc := formatSourceLocation baseOffset m + let formatted := formatExpressionOnly prog expr + IO.println s!" └─ {exprLoc}: {MSG_IMPOSSIBLE} {formatted}" + IO.println s!" {MSG_UNDER_ASSUMPTIONS}" + for expr in result.context.pathCondition.reverse do + -- Flatten conjunctions to show each on separate line + for conjunct in flattenConjunction expr do + let formatted := formatExpressionOnly prog conjunct + IO.println s!" {formatted}" + | _ => pure () + | none => + -- No diagnosis - use same format with └─ + if !result.context.pathCondition.isEmpty then + match stmt with + | .check m expr | .assert m expr => + let exprLoc := formatSourceLocation baseOffset m + let formatted := formatExpressionOnly prog expr + IO.println s!" └─ {exprLoc}: {MSG_COULD_NOT_PROVE} {formatted}" + IO.println s!" {MSG_UNDER_ASSUMPTIONS}" + for expr in result.context.pathCondition.reverse do + -- Flatten conjunctions to show each on separate line + for conjunct in flattenConjunction expr do + let formatted := formatExpressionOnly prog conjunct + IO.println s!" {formatted}" + | .reach m expr => + let exprLoc := formatSourceLocation baseOffset m + let formatted := formatExpressionOnly prog expr + IO.println s!" └─ {exprLoc}: {MSG_IMPOSSIBLE} {formatted}" + IO.println s!" {MSG_UNDER_ASSUMPTIONS}" + for expr in result.context.pathCondition.reverse do + -- Flatten conjunctions to show each on separate line + for conjunct in flattenConjunction expr do + let formatted := formatExpressionOnly prog conjunct + IO.println s!" {formatted}" + | _ => pure () + | _ => pure () + +--------------------------------------------------------------------- +-- Example from Verifier.lean Documentation +--------------------------------------------------------------------- + +/-- +info: Statement: check 8 == 8 && f(5) == 7 +✗ Unknown + Path condition: + forall x : int pattern f(x) f(x) == x + 1 + Found 1 diagnosed failures +Failing expression: f(5) == 7 +✗ Refuted (proved false/unreachable) + Path condition: + 8 == 8 + forall x : int pattern f(x) f(x) == x + 1 +-/ +#guard_msgs in +#eval exampleVerification + +--------------------------------------------------------------------- +-- Check Statement Tests +--------------------------------------------------------------------- + +/-- +info: test_checks_are_not_learned: ✗ unknown + (0,113): check f(5) > 1 + └─ (0,113): could not prove f(5) > 1 + under the assumptions + forall x : int pattern f(x) f(x) > 0 +test_checks_are_not_learned: ✗ unknown + (0,130): check f(5) > 1 + └─ (0,130): could not prove f(5) > 1 + under the assumptions + forall x : int pattern f(x) f(x) > 0 +-/ +#guard_msgs in +#eval testVerification $ #strata program B3CST; +function f(x : int) : int +axiom forall x : int pattern f(x) f(x) > 0 +procedure test_checks_are_not_learned() { + check f(5) > 1 + check f(5) > 1 +} +#end + +/-- +info: test: ✓ verified +-/ +#guard_msgs in +#eval testVerification $ #strata program B3CST; +function f(x : int) : int +axiom forall x : int pattern f(x) x > 0 ==> f(x) > 0 +procedure test() { + check 5 > 0 ==> f(5) > 0 +} +#end + +/-- +info: test_fail: ✗ counterexample found + (0,52): check 5 == 5 && f(5) == 10 + └─ (0,68): could not prove f(5) == 10 + under the assumptions + 5 == 5 +-/ +#guard_msgs in +#eval testVerification $ #strata program B3CST; +function f(x : int) : int +procedure test_fail() { + check 5 == 5 && f(5) == 10 +} +#end + + +/-- +info: test_all_expressions: ✗ unknown + (0,127): check (false || true) && (if true true else false) && f(5) && notalwaystrue(1, 2) && 5 == 5 && !(3 == 4) && 2 < 3 && 2 <= 2 && 4 > 3 && 4 >= 4 && 1 + 2 == 4 && 5 - 2 == 3 && 3 * 4 == 12 && 10 div 2 == 5 && 7 mod 3 == 1 && -(5) == 0 - 5 && notalwaystrue(3, 4) && (true ==> true) && (forall y : int pattern f(y) f(y) || !f(y)) && (forall y : int y > 0 || y <= 0) + └─ (0,213): could not prove notalwaystrue(1, 2) + under the assumptions + forall x : int pattern f(x) f(x) == (x + 1 == 6) + false || true + if true true else false + f(5) + └─ (0,353): it is impossible that 1 + 2 == 4 + under the assumptions + forall x : int pattern f(x) f(x) == (x + 1 == 6) + false || true + if true true else false + f(5) + notalwaystrue(1, 2) + 5 == 5 + !(3 == 4) + 2 < 3 + 2 <= 2 + 4 > 3 + 4 >= 4 +-/ +#guard_msgs in +#eval testVerification $ #strata program B3CST; +function f(x : int) : bool { x + 1 == 6 } +function notalwaystrue(a : int, b : int) : bool +procedure test_all_expressions() { + check (false || true) && + (if true true else false) && + f(5) && + notalwaystrue(1, 2) && + 5 == 5 && + !(3 == 4) && + 2 < 3 && + 2 <= 2 && + 4 > 3 && + 4 >= 4 && + 1 + 2 == 4 && // The second error that should be spot + 5 - 2 == 3 && + 3 * 4 == 12 && + 10 div 2 == 5 && + 7 mod 3 == 1 && + -5 == 0 - 5 && + notalwaystrue(3, 4) && // Not an error because we assumed false + (true ==> true) && + (forall y : int pattern f(y) f(y) || !f(y)) && + (forall y : int y > 0 || y <= 0) +} +#end + +--------------------------------------------------------------------- +-- Assert Statement Tests +--------------------------------------------------------------------- + +-- Assertions are assumed so further checks pass +/-- +info: test_assert_helps: ✗ unknown + (0,103): assert f(5) > 1 + └─ (0,103): could not prove f(5) > 1 + under the assumptions + forall x : int pattern f(x) f(x) > 0 +test_assert_helps: ✓ verified +-/ +#guard_msgs in +#eval testVerification $ #strata program B3CST; +function f(x : int) : int +axiom forall x : int pattern f(x) f(x) > 0 +procedure test_assert_helps() { + assert f(5) > 1 + check f(5) > 1 +} +#end + +/-- +info: test_assert_with_trace: ✗ unknown + (0,138): assert f(5) > 10 + └─ (0,138): could not prove f(5) > 10 + under the assumptions + forall x : int pattern f(x) f(x) > 0 + f(1) > 0 + f(4) > 0 +-/ +#guard_msgs in +#eval testVerification $ #strata program B3CST; +function f(x : int) : int +axiom forall x : int pattern f(x) f(x) > 0 +procedure test_assert_with_trace() { + assume f(1) > 0 && f(4) > 0 + assert f(5) > 10 +} +#end + +--------------------------------------------------------------------- +-- Reach Statement Tests +--------------------------------------------------------------------- + +/-- +info: test_reach_bad: ✗ refuted + (0,100): reach f(5) < 0 + └─ (0,100): it is impossible that f(5) < 0 + under the assumptions + forall x : int pattern f(x) f(x) > 0 +-/ +#guard_msgs in +#eval testVerification $ #strata program B3CST; +function f(x : int) : int +axiom forall x : int pattern f(x) f(x) > 0 +procedure test_reach_bad() { + reach f(5) < 0 +} +#end + +/-- +info: test_reach_good: ✓ reachability unknown +-/ +#guard_msgs in +#eval testVerification $ #strata program B3CST; +function f(x : int) : int +axiom forall x : int pattern f(x) f(x) > 0 +procedure test_reach_good() { + reach f(5) > 5 +} +#end + +/-- +info: test_reach_with_trace: ✗ refuted + (0,137): reach f(5) < 0 + └─ (0,137): it is impossible that f(5) < 0 + under the assumptions + forall x : int pattern f(x) f(x) > 0 + f(1) > 0 + f(4) > 0 +-/ +#guard_msgs in +#eval testVerification $ #strata program B3CST; +function f(x : int) : int +axiom forall x : int pattern f(x) f(x) > 0 +procedure test_reach_with_trace() { + assume f(1) > 0 && f(4) > 0 + reach f(5) < 0 +} +#end + +--------------------------------------------------------------------- +-- Automatic Diagnosis Tests +--------------------------------------------------------------------- + +/-- +info: test_reach_diagnosis: ✗ refuted + (0,106): reach f(5) > 5 && f(5) < 0 + └─ (0,124): it is impossible that f(5) < 0 + under the assumptions + forall x : int pattern f(x) f(x) > 0 + f(5) > 5 +-/ +#guard_msgs in +#eval testVerification $ #strata program B3CST; +function f(x : int) : int +axiom forall x : int pattern f(x) f(x) > 0 +procedure test_reach_diagnosis() { + reach f(5) > 5 && f(5) < 0 +} +#end + + + +/-- +info: test_all_expressions: ✗ refuted + (0,127): reach (false || true) && (if true true else false) && f(5) && notalwaystrue(1, 2) && 5 == 5 && !(3 == 4) && 2 < 3 && 2 <= 2 && 4 > 3 && 4 >= 4 && 1 + 2 == 4 && 5 - 2 == 3 && 3 * 4 == 12 && 10 div 2 == 5 && 7 mod 3 == 1 && -(5) == 0 - 5 && notalwaystrue(3, 4) && (true ==> true) && (forall y : int pattern f(y) f(y) || !f(y)) && (forall y : int y > 0 || y <= 0) + └─ (0,353): it is impossible that 1 + 2 == 4 + under the assumptions + forall x : int pattern f(x) f(x) == (x + 1 == 6) + false || true + if true true else false + f(5) + notalwaystrue(1, 2) + 5 == 5 + !(3 == 4) + 2 < 3 + 2 <= 2 + 4 > 3 + 4 >= 4 +-/ +#guard_msgs in +#eval testVerification $ #strata program B3CST; +function f(x : int) : bool { x + 1 == 6 } +function notalwaystrue(a : int, b : int) : bool +procedure test_all_expressions() { + reach (false || true) && + (if true true else false) && + f(5) && + notalwaystrue(1, 2) && + 5 == 5 && + !(3 == 4) && + 2 < 3 && + 2 <= 2 && + 4 > 3 && + 4 >= 4 && + 1 + 2 == 4 && // First unreachable - diagnosis stops here + 5 - 2 == 3 && + 3 * 4 == 12 && + 10 div 2 == 5 && + 7 mod 3 == 1 && + -5 == 0 - 5 && + notalwaystrue(3, 4) && + (true ==> true) && + (forall y : int pattern f(y) f(y) || !f(y)) && + (forall y : int y > 0 || y <= 0) +} +#end + + + +/-- +info: test_all_expressions: ✗ refuted + (0,85): reach notalwaystrue(1, 2) && !notalwaystrue(1, 2) && 5 == 4 + └─ (0,122): it is impossible that !notalwaystrue(1, 2) + under the assumptions + notalwaystrue(1, 2) +-/ +#guard_msgs in +#eval testVerification $ #strata program B3CST; +function notalwaystrue(a : int, b : int) : bool +procedure test_all_expressions() { + reach notalwaystrue(1, 2) && + !notalwaystrue(1, 2) && + 5 == 4 +} +#end +end B3.Verifier.Tests diff --git a/StrataVerify.lean b/StrataVerify.lean index ff7aef04..0f3f2449 100644 --- a/StrataVerify.lean +++ b/StrataVerify.lean @@ -7,6 +7,7 @@ -- Executable for verifying a Strata program from a file. import Strata.Languages.Boogie.Verifier import Strata.Languages.C_Simp.Verify +import Strata.Languages.B3.Verifier.Program import Strata.Util.IO import Std.Internal.Parsec @@ -31,7 +32,7 @@ def parseOptions (args : List String) : Except Std.Format (Options × String) := | _, args => .error f!"Unknown options: {args}" def usageMessage : Std.Format := - f!"Usage: StrataVerify [OPTIONS] {Std.Format.line}\ + f!"Usage: StrataVerify [OPTIONS] {Std.Format.line}\ {Std.Format.line}\ Options:{Std.Format.line}\ {Std.Format.line} \ @@ -51,6 +52,7 @@ def main (args : List String) : IO UInt32 := do let dctx := Elab.LoadedDialects.builtin let dctx := dctx.addDialect! Boogie let dctx := dctx.addDialect! C_Simp + let dctx := dctx.addDialect! B3CST let leanEnv ← Lean.mkEmptyEnvironment 0 match Strata.Elab.elabProgram dctx leanEnv inputCtx with | .ok pgm => @@ -74,6 +76,27 @@ def main (args : List String) : IO UInt32 := do let vcResults ← try if file.endsWith ".csimp.st" then C_Simp.verify "z3" pgm opts + else if file.endsWith ".b3.st" || file.endsWith ".b3cst.st" then + -- B3 verification (different model, handle inline) + let ast ← match B3.Verifier.programToB3AST pgm with + | Except.error msg => throw (IO.userError s!"Failed to convert to B3 AST: {msg}") + | Except.ok ast => pure ast + let solver ← B3.Verifier.createInteractiveSolver "z3" + let reports ← B3.Verifier.programToSMT ast solver + -- B3 uses a different result format, print directly and return empty array + for report in reports do + IO.println s!"\nProcedure: {report.procedureName}" + for (result, _) in report.results do + let marker := if result.result.isError then "✗" else "✓" + let desc := match result.result with + | .error .counterexample => "counterexample found" + | .error .unknown => "unknown" + | .error .refuted => "refuted" + | .success .verified => "verified" + | .success .reachable => "reachable" + | .success .reachabilityUnknown => "reachability unknown" + IO.println s!" {marker} {desc}" + pure #[] -- Return empty array since B3 prints directly else verify "z3" pgm inputCtx opts catch e =>