From 89c5528c498d277854799a740bca417e907f9d87 Mon Sep 17 00:00:00 2001 From: Lydia Kondylidou <33327056+kondylidou@users.noreply.github.com> Date: Thu, 16 Jul 2026 15:04:44 +0200 Subject: [PATCH] feat(Core): nat/pos counterexample support via UF+axioms re-query MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add candidate-model propagation and axiom-drop re-query so nat/pos verification failures surface concrete counterexamples instead of stopping at `unknown`. Key changes: - SMTUtils: parse cvc5 candidate model on `unknown` result; use actual user-variable SMT terms (from estate.functions) in incremental solver get-value calls instead of boolean assumption IDs, so nat/pos variable values are retrievable - Verifier: preserve `unknown (some m)` payload across SMT.Result.merge; extract candidate model from `unknown (some m)` in getObligationResult; add VCResult.hasValidityUnknown (weaker gate than isUnknown, catches satisfiableValidityUnknown outcomes from nat VCs with bridge axioms); add requeryDropAxioms parameter to verify — strips named axiom assumes from oblProgram and re-runs unknown obligations so the solver can certify a counterexample unimpeded by universally-quantified bridge axioms - VerifierProofs: update merge_kind proof for new unknown×unknown model-preserving branches - lake-manifest: bump StrataDDM to 4ea13cd (adds @[noExponent] arg-level format marker needed by Strata/DL/SMT/DDMTransform/Parse.lean) Co-Authored-By: Claude Sonnet 4.6 --- Strata/DL/Imperative/SMTUtils.lean | 24 +++++-- Strata/Languages/Core/Verifier.lean | 77 +++++++++++++++++++++-- Strata/Languages/Core/VerifierProofs.lean | 6 +- 3 files changed, 95 insertions(+), 12 deletions(-) diff --git a/Strata/DL/Imperative/SMTUtils.lean b/Strata/DL/Imperative/SMTUtils.lean index 440c8e3172..3bc9bb9ea3 100644 --- a/Strata/DL/Imperative/SMTUtils.lean +++ b/Strata/DL/Imperative/SMTUtils.lean @@ -254,7 +254,11 @@ def solverResult {P : PureExpr} [ToFormat P.Ident] | .ok model => return some (.sat model, skipToNextVerdict rest) | .error _ => return some (.sat [], skipToNextVerdict rest) | "unsat" => return some (.unsat, skipToNextVerdict rest) - | "unknown" => return some (.unknown, skipToNextVerdict rest) + | "unknown" => + let rawModel ← parseModelDDM rest + match (processModel typedVarToSMTFn vars rawModel E) with + | .ok model => return some (.unknown (some model), skipToNextVerdict rest) + | .error _ => return some (.unknown, skipToNextVerdict rest) | _ => return none let mkError (output : IO.Process.Output) : SolverError := @@ -319,12 +323,22 @@ def dischargeObligationIncremental {P : PureExpr} [ToFormat P.Ident] [BEq P.Iden let action : Strata.SMT.IncrementalSolverM (Except SolverError (Result P.Ident × Result P.Ident × Strata.SMT.EncoderState)) := do let solver := Strata.SMT.IncrementalSolver.mkIncrementalSolver - let { obligationId, assumptionIds, estate } ← encodeDecl solver - let varIds := assumptionIds.map fun id => Strata.SMT.Term.var ⟨id, .bool⟩ + let { obligationId, assumptionIds := _, estate } ← encodeDecl solver + -- Build SMT terms for actual user variables (not boolean assumption IDs) + -- so get-value returns nat/pos values the candidate phase can validate. + let userVarTerms : List Strata.SMT.Term := + vars.filterMap fun (var, ty) => + match typedVarToSMTFn var ty with + | .error _ => none + | .ok (smtName, termType) => + let key : Strata.SMT.UF := { id := smtName, args := [], out := termType } + match estate.functions[key]? with + | none => none + | some encodedId => some (Strata.SMT.Term.var ⟨encodedId, termType⟩) let getModelForVars : Strata.SMT.IncrementalSolverM (Model P.Ident) := do - if varIds.isEmpty then return [] + if userVarTerms.isEmpty then return [] try - let pairs ← solver.getValue varIds + let pairs ← solver.getValue userVarTerms match pairs with | [(.prim (.string rawOutput), _)] => let rawModel ← parseModelDDM rawOutput diff --git a/Strata/Languages/Core/Verifier.lean b/Strata/Languages/Core/Verifier.lean index f7d36acc2a..77fea37d93 100644 --- a/Strata/Languages/Core/Verifier.lean +++ b/Strata/Languages/Core/Verifier.lean @@ -1162,6 +1162,8 @@ def SMT.Result.merge (a b : SMT.Result) : SMT.Result := | _, .err e => .err e | .sat m, _ => .sat m | _, .sat m => .sat m + | .unknown (some m), .unknown _ => .unknown (some m) + | .unknown _, .unknown (some m) => .unknown (some m) | .unknown m, _ => .unknown m | _, .unknown m => .unknown m | .unsat, .unsat => .unsat @@ -1294,6 +1296,14 @@ def VCResult.isUnknown (vr : VCResult) : Bool := | .ok o => o.isUnknown | .error _ => false +-- Weaker gate for requeryDropAxioms: triggers when validity is unknown regardless +-- of satisfiability. Nat VCs land in satisfiableValidityUnknown (sat + unknown_validity) +-- so VCResult.isUnknown (which requires both unknown) misses them. +def VCResult.hasValidityUnknown (vr : VCResult) : Bool := + match vr.outcome with + | .ok o => match o.validityProperty with | .unknown _ => true | _ => false + | .error _ => false + def VCResult.isImplementationError (vr : VCResult) : Bool := match vr.outcome with | .error (.encoding _) | .error (.solverCrash _) => true @@ -1645,11 +1655,16 @@ def getObligationResult (assumptionTerms : List Term) (obligationTerm : Term) validityProperty := adjVal, solverLog := #[smtLog] } let outcome := maskOutcome rawOutcome satisfiabilityCheck validityCheck - -- Extract model from sat results (using raw solver results) + -- Extract model from sat or unknown-with-candidate results. + -- unknown (some m) arises when the solver returns a candidate model it cannot + -- certify (e.g. cvc5 with quantified bridge axioms). Phases may promote it + -- to sat; we still want the model available for display. let model := match satResult, validityResult with - | .sat m, _ => convertModel m (SMT.Context.getConstructorNames ctx) - | _, .sat m => convertModel m (SMT.Context.getConstructorNames ctx) - | _, _ => [] + | .sat m, _ => convertModel m (SMT.Context.getConstructorNames ctx) + | _, .sat m => convertModel m (SMT.Context.getConstructorNames ctx) + | .unknown (some m), _ => convertModel m (SMT.Context.getConstructorNames ctx) + | _, .unknown (some m) => convertModel m (SMT.Context.getConstructorNames ctx) + | _, _ => [] -- Filter out managed variables from model display let managedVarNames := (varDefinitions.map (·.name)) ++ (varDeclarations.map (·.name)) let model := model.filter fun (name, _) => !managedVarNames.contains name.name @@ -1939,6 +1954,10 @@ def verify (program : Program) (solver : Option CoreSMTSolver := none) (mkDischarge : MkDischargeFn := mkDischargeFn) (pipelineCtx : Option PipelineContext := none) + -- Axiom names to strip on a re-query when obligations remain unknown after + -- the primary pass. Sound only when the named axioms are consequences of + -- the remaining definitions (any sat model satisfies them automatically). + (requeryDropAxioms : List String := []) : EIO DiagnosticModel VCResults := do let profile := options.profile let pctx ← match pipelineCtx with @@ -1976,7 +1995,55 @@ def verify (program : Program) if profile then let _ ← (IO.println allStats.format |>.toBaseIO) let results : VCResults := (VCss.map (·.fst)).toArray.flatten - .ok results.mergeByAssertion + let merged := results.mergeByAssertion + -- Re-query pass: if the caller specified axioms to drop and any obligation is + -- still unknown, re-run those obligations without those axioms so the solver + -- can return a certified sat (counterexample) unimpeded by the universals. + if requeryDropAxioms.isEmpty || !merged.any (·.hasValidityUnknown) then + return merged + -- Bridge axioms live in `program` (the original input); `oblProgram` already + -- excludes them because `toCoreProofObligationProgram` only keeps .type decls, + -- eval-derived functions, distinct constraints, and obligation procedures. + -- Check existence against `program.decls` so mis-spelled names still warn. + let programAxiomNames := program.decls.filterMap fun d => d.getAxiom?.map (·.name) + let matchedAxioms := requeryDropAxioms.filter (programAxiomNames.contains ·) + if matchedAxioms.isEmpty then + let _ ← IO.println s!"[Strata] requeryDropAxioms: none of {requeryDropAxioms} matched any axiom declaration — re-query skipped" |>.toBaseIO + return merged + -- Bridge axioms were baked into `oblProgram`'s procedure bodies as `assume` + -- statements by `toCoreProofObligationProgram`. Strip those assumes so the + -- re-query SMT problem is axiom-free and cvc5 can certify a counterexample. + let oblProgramNoAxioms : Program := + { oblProgram with + decls := oblProgram.decls.map fun d => + match d with + | .proc p md => + let newBody := match p.body with + | .structured ss => + .structured (ss.filter fun s => + match s with + | .cmd (.cmd (.assume label _ _)) => !matchedAxioms.contains label + | _ => true) + | other => other + .proc { p with body := newBody } md + | other => other } + let requerySolver := mkDefaultCoreSMTSolver options counter tempDir axiomCache? + axiomNames (axiomProgram := program) externalPhases phases + (mkDischarge := mkDischarge) pctx + let (reQueryVCs, _) ← pctx.withPhase "requeryVcDischarge" do + requerySolver moreFns oblProgramNoAxioms + let reQueryMerged := reQueryVCs.mergeByAssertion + -- Build an index for O(n) lookup instead of O(n²) linear scan per unknown. + let reQueryIndex : Std.HashMap String VCResult := + reQueryMerged.foldl (fun acc r => acc.insert r.obligation.label r) {} + -- Only upgrade unknown → failure; never treat a re-query unsat as a proof + -- (the dropped axioms might have been load-bearing for the unsat direction). + return merged.map fun r => + if !r.hasValidityUnknown then r + else + match reQueryIndex.get? r.obligation.label with + | some r2 => if r2.isFailure then r2 else r + | none => r end -- public section end Core diff --git a/Strata/Languages/Core/VerifierProofs.lean b/Strata/Languages/Core/VerifierProofs.lean index 1bc4564f4a..91324824a2 100644 --- a/Strata/Languages/Core/VerifierProofs.lean +++ b/Strata/Languages/Core/VerifierProofs.lean @@ -132,5 +132,7 @@ theorem ResultKind.merge_le {a b c : ResultKind} (ha : a ≤ c) (hb : b ≤ c) : above transfer to the concrete function at the kind level. -/ theorem merge_kind (a b : Core.SMT.Result) : (a.merge b).toKind = a.toKind.merge b.toKind := by - unfold Core.SMT.Result.merge - cases a <;> cases b <;> rfl + -- The unknown×unknown case requires a payload split on both Option fields + -- since the new model-preserving branches pattern-match on Some/None. + cases a <;> cases b <;> simp [Core.SMT.Result.merge, Core.SMT.Result.toKind, ResultKind.merge] <;> + (try (rename_i m₁ m₂; cases m₁ <;> cases m₂ <;> rfl))