verify: Confirm certified counterexamples in Lean, and make the gate's Lean row decisive

clang/lib/Verify/Backend/Certify.cpp

@@ -4150,6 +4150,22 @@ void sourceVariables(const LogicExpr *Expr, std::set<std::string> &Bound,
 }
 } // namespace
 
+std::shared_ptr<const CounterexampleAssignment>
+verify::counterexampleAssignment(const Obligation &Item,
+                                 CandidateModel &Model) {
+  std::vector<std::pair<std::string, LogicSort>> Variables;
+  std::set<std::string> Bound;
+  sourceVariables(Item.Goal.get(), Bound, Variables);
+  auto Assignment = std::make_shared<CounterexampleAssignment>();
+  for (const auto &[Name, Sort] : Variables) {
+    std::optional<LogicValue> Given = Model.constant(Name, Sort);
+    if (!Given)
+      return nullptr;
+    Assignment->Values.emplace(Name, std::move(*Given));
+  }
+  return Assignment;
+}
+
 std::vector<VerifyModelValue>
 verify::candidateValues(const ObligationModule &Module, const LogicExpr &Query,
                         CandidateModel &Model) {

clang/lib/Verify/Backend/Certify.h

@@ -232,6 +232,18 @@ std::optional<LogicValue> evaluateTerm(const ObligationModule &Module,
                                        const CertifyLimits &Limits = {},
                                        std::string *Failure = nullptr);
 
+/// The values a certified counterexample gives the free variables of the goal
+/// of the obligation it fails, by name: what a refutation of that goal
+/// applies it to.
+struct CounterexampleAssignment {
+  std::map<std::string, LogicValue> Values;
+};
+
+/// The assignment \p Model gives the free variables of \p Item's goal, or
+/// null when it gives one no value.
+std::shared_ptr<const CounterexampleAssignment>
+counterexampleAssignment(const Obligation &Item, CandidateModel &Model);
+
 /// The source variables of \p Query with the values \p Model gives them, as
 /// a counterexample shows them; no value where the model gives none.
 std::vector<VerifyModelValue> candidateValues(const ObligationModule &Module,