Extend pool-based quantifier instantiation to axioms; add diagnostic …

Source/BoogieDriver/BoogieDriver.cs

@@ -78,6 +78,11 @@ public static int Main(string[] args)
         options.XmlSink.Close();
       }
 
+      if (options.JsonSink != null)
+      {
+        options.JsonSink.Close();
+      }
+
       if (options.Wait)
       {
         Console.WriteLine("Press Enter to exit.");

Source/Core/CoreOptions.cs

@@ -109,6 +109,9 @@ public enum VerbosityLevel
     double VcsPathJoinMult { get; }
     bool VerifySeparately { get; }
     bool KeepQuantifier { get; }
+    bool PoolTrace { get; }
+    bool PoolSummary { get; }
+    JsonSink JsonSink { get; }
 
     public enum ProverWarnings
     {

Source/Core/JsonSink.cs

@@ -0,0 +1,104 @@
+using System;
+using System.IO;
+using System.Text.Json;
+using System.Text.Json.Nodes;
+
+namespace Microsoft.Boogie
+{
+  // /jsonOutput:<file> — writes one structured JSON document per Boogie run,
+  // with per-implementation verification results. Designed for tooling / AI
+  // consumers that want a stable machine-readable surface.
+  //
+  // Schema (v1):
+  // {
+  //   "boogieVersion": "3.x.x",
+  //   "commandLine": "...",
+  //   "implementations": [
+  //     {
+  //       "name": "Foo",
+  //       "location": { "file": "...", "line": 12, "column": 5 },
+  //       "outcome": "Correct" | "Errors" | "TimedOut" | ...,
+  //       "durationMs": 1234.5,
+  //       "resourceCount": 1000,
+  //       "errors": [
+  //         { "message": "...", "location": { "file": ..., "line": ..., "column": ... } }
+  //       ]
+  //     }
+  //   ]
+  // }
+  public sealed class JsonSink
+  {
+    private readonly string filename; // "-" means options.OutputWriter
+    private readonly CoreOptions options;
+    private readonly JsonObject root = new();
+    private readonly JsonArray implementations = new();
+    private readonly object gate = new();
+
+    public JsonSink(CoreOptions options, string filename)
+    {
+      this.filename = filename;
+      this.options = options;
+      root["boogieVersion"] = options.VersionNumber;
+      root["commandLine"] = Environment.CommandLine;
+      root["implementations"] = implementations;
+    }
+
+    public readonly struct ErrorRecord
+    {
+      public readonly string Message;
+      public readonly IToken Tok;
+      public ErrorRecord(string message, IToken tok) { Message = message; Tok = tok; }
+    }
+
+    public void WriteImplementationResult(string name, IToken tok, string outcome,
+      double durationMs, int resourceCount, System.Collections.Generic.IEnumerable<ErrorRecord> errors)
+    {
+      var obj = new JsonObject
+      {
+        ["name"] = name,
+        ["location"] = LocationOf(tok),
+        ["outcome"] = outcome,
+        ["durationMs"] = durationMs,
+        ["resourceCount"] = resourceCount
+      };
+      var errorArr = new JsonArray();
+      foreach (var e in errors)
+      {
+        errorArr.Add(new JsonObject
+        {
+          ["message"] = e.Message,
+          ["location"] = LocationOf(e.Tok)
+        });
+      }
+      obj["errors"] = errorArr;
+      lock (gate)
+      {
+        implementations.Add(obj);
+      }
+    }
+
+    public void Close()
+    {
+      var json = root.ToJsonString(new JsonSerializerOptions { WriteIndented = true });
+      if (filename == "-")
+      {
+        options.OutputWriter.WriteLine(json);
+        options.OutputWriter.Flush();
+      }
+      else
+      {
+        File.WriteAllText(filename, json);
+      }
+    }
+
+    private static JsonObject LocationOf(IToken tok)
+    {
+      return new JsonObject
+      {
+        ["file"] = tok?.filename ?? "<unknown>",
+        ["line"] = tok?.line ?? 0,
+        ["column"] = tok?.col ?? 0
+      };
+    }
+  }
+}

Source/ExecutionEngine/CommandLineOptions.cs

@@ -210,6 +210,8 @@ public bool PrintWithUniqueASTIds {
 
     private string XmlSinkFilename { get; set; }
     [Peer] public XmlSink XmlSink { get; set; }
+    public JsonSink JsonSink { get; set; }
+    private string JsonSinkFilename { get; set; }
     public bool Wait { get; set; }
 
     public bool Trace => Verbosity == CoreOptions.VerbosityLevel.Trace;
@@ -559,6 +561,16 @@ public bool KeepQuantifier {
       set => keepQuantifier = value;
     }
 
+    public bool PoolTrace {
+      get => poolTrace;
+      set => poolTrace = value;
+    }
+
+    public bool PoolSummary {
+      get => poolSummary;
+      set => poolSummary = value;
+    }
+
     public HashSet<string> Libraries { get; set; } = new HashSet<string>();
 
     // Note that procsToCheck stores all patterns <p> supplied with /proc:<p>
@@ -609,6 +621,8 @@ void ObjectInvariant5()
     private bool normalizeNames;
     private bool normalizeDeclarationOrder = true;
     private bool keepQuantifier = false;
+    private bool poolTrace = false;
+    private bool poolSummary = false;
 
     public List<CoreOptions.ConcurrentHoudiniOptions> Cho { get; set; } = new();
 
@@ -701,6 +715,14 @@ protected override bool ParseOption(string name, CommandLineParseState ps)
 
           return true;
 
+        case "jsonOutput":
+          if (ps.ConfirmArgumentCount(1))
+          {
+            JsonSinkFilename = args[ps.i];
+          }
+
+          return true;
+
         case "printPruned":
         case "printSplit":
           if (ps.ConfirmArgumentCount(1))
@@ -1390,7 +1412,9 @@ protected override bool ParseOption(string name, CommandLineParseState ps)
               ps.CheckBooleanFlag("useBaseNameForFileName", x => UseBaseNameForFileName = x) ||
               ps.CheckBooleanFlag("freeVarLambdaLifting", x => FreeVarLambdaLifting = x) ||
               ps.CheckBooleanFlag("warnNotEliminatedVars", x => WarnNotEliminatedVars = x) ||
-              ps.CheckBooleanFlag("keepQuantifier", x => keepQuantifier = x)
+              ps.CheckBooleanFlag("keepQuantifier", x => keepQuantifier = x) ||
+              ps.CheckBooleanFlag("poolTrace", x => poolTrace = x) ||
+              ps.CheckBooleanFlag("poolSummary", x => poolSummary = x)
           )
           {
             // one of the boolean flags matched
@@ -1422,6 +1446,11 @@ public override void ApplyDefaultOptions()
         XmlSink = new XmlSink(this, XmlSinkFilename);
       }
 
+      if (JsonSinkFilename != null)
+      {
+        JsonSink = new JsonSink(this, JsonSinkFilename);
+      }
+
       if (printErrorModelFile != null) {
         ModelWriter = new StreamWriter(printErrorModelFile, false);
       }
@@ -2019,6 +2048,27 @@ not covered by a proof.
                 If pool-based quantifier instantiation creates instances of a quantifier
                 then keep the quantifier along with the instances. By default, the quantifier
                 is dropped if any instances are created.
+                For pool-bearing axioms (non-lambda-definition), the same rule applies
+                symmetrically: by default the axiom is dropped from the prover context and
+                survives only as its pool-instantiated ground forms in the VC antecedent;
+                with /keepQuantifier the axiom is kept in the prover context as usual.
+  /poolTrace
+                Emit diagnostics about pool-based quantifier instantiation as each
+                implementation is verified: which pool received which values, how
+                many instances each factorized quantifier produced, and which
+                candidate instances were dropped due to pool-type mismatches.
+                Useful for debugging why a {:pool ...} annotation did not fire.
+  /poolSummary
+                At the start of verification, print a summary: count of axioms
+                (total, pool-bearing, lambda-definition, plain); count of
+                quantifiers (total, pool-bearing, polymorphic); and the pool names
+                referenced in the program, with their producer/consumer locations.
+                Useful for auditing pool annotations across a program.
+  /jsonOutput:<file>
+                Write a structured JSON document summarising the verification run:
+                per-implementation outcome, duration, resource count, and errors
+                with source locations. Use '-' as the filename to write to stdout.
+                Intended for programmatic / AI consumers.
 
   ---- Verification-condition splitting --------------------------------------
 

Source/ExecutionEngine/ExecutionEngine.cs

@@ -590,6 +590,12 @@ public async Task<PipelineOutcome> InferAndVerify(
         action(Options, processedProgram);
       }
 
+      if (Options.PoolSummary)
+      {
+        PoolSummary.Emit(processedProgram.Program, Options.OutputWriter);
+        Options.OutputWriter.Flush();
+      }
+
       if (!Options.Verify)
       {
         return PipelineOutcome.Done;
@@ -767,6 +773,7 @@ private async Task<PipelineOutcome> VerifyEachImplementation(TextWriter outputWr
         await Task.WhenAll(tasks);
         foreach (var task in tasks) {
           task.Result.ProcessXml(this);
+          task.Result.ProcessJson(this);
         }
       } catch(TaskCanceledException) {
         outcome = PipelineOutcome.Cancelled;

Source/ExecutionEngine/ImplementationRunResult.cs

@@ -68,6 +68,54 @@ public String GetOutput(OutputPrinter printer,
     return result.ToString();
   }
 
+  public void ProcessJson(ExecutionEngine engine) {
+    var sink = engine.Options.JsonSink;
+    if (sink == null) { return; }
+    var errors = Errors.Select(ExtractError);
+    sink.WriteImplementationResult(
+      implementation.VerboseName,
+      implementation.tok,
+      VcOutcome.ToString().ToLowerInvariant(),
+      Elapsed.TotalMilliseconds,
+      ResourceCount,
+      errors);
+  }
+
+  private JsonSink.ErrorRecord ExtractError(Counterexample cex) {
+    // Each Counterexample subtype reports a different failure shape.
+    IToken tok;
+    string msg;
+    switch (cex) {
+      case CallCounterexample call:
+        // Precondition violation at a call site.
+        tok = call.FailingCall.tok;
+        msg = call.FailingRequires.ErrorMessage
+              ?? call.FailingRequires.Description?.FailureDescription
+              ?? "a precondition could not be proved";
+        break;
+      case ReturnCounterexample ret:
+        // Postcondition violation at a return site.
+        tok = ret.FailingReturn.tok;
+        msg = ret.FailingEnsures.ErrorMessage
+              ?? ret.FailingEnsures.Description?.FailureDescription
+              ?? "a postcondition could not be proved";
+        break;
+      case AssertCounterexample asrt:
+        tok = asrt.FailingAssert.tok;
+        msg = asrt.FailingAssert.ErrorMessage
+              ?? asrt.FailingAssert.Description?.FailureDescription
+              ?? "this assertion could not be proved";
+        break;
+      default:
+        tok = cex.FailingAssert?.tok ?? implementation.tok;
+        msg = cex.FailingAssert?.ErrorMessage
+              ?? cex.FailingAssert?.Description?.FailureDescription
+              ?? "verification failed";
+        break;
+    }
+    return new JsonSink.ErrorRecord(msg, tok);
+  }
+
   public void ProcessXml(ExecutionEngine engine) {
     if (engine.Options.XmlSink == null) {
       return;