Add goal printing flags (-upto, -lastgoals) and LLM agent guide

Add two new flags for the `easycrypt` CLI to support LLM coding agents:
- `-upto <pos>`: compile up to a given position and print goals there
- `-lastgoals`: print the last unproven goals

Also add a dedicated `llm` command mode and an LLM agent guide
(doc/llm/CLAUDE.md) documenting EasyCrypt tactics and workflow for
use with AI coding assistants.

Author: strub

doc/llm/CLAUDE.md

@@ -0,0 +1,149 @@
+# EasyCrypt — LLM Agent Guide
+
+EasyCrypt is a proof assistant for reasoning about the security of
+cryptographic constructions. It provides support for probabilistic
+computations, program logics (Hoare logic, probabilistic Hoare logic,
+probabilistic relational Hoare logic), and ambient mathematical
+reasoning.
+
+## Using the `llm` command
+
+The `llm` subcommand is designed for non-interactive, LLM-friendly
+batch compilation. It produces no progress bar and no `.eco` cache
+files.
+
+```
+easycrypt llm [OPTIONS] FILE.ec
+```
+
+### Options
+
+- `-upto LINE` or `-upto LINE:COL` — Compile up to (but not
+  including) the given location, then print the current goal state to
+  stdout and exit with code 0. Use this to inspect the proof state at
+  a specific point in a file.
+
+- `-lastgoals` — On failure, print the goal state (as it was just
+  before the failing command) to stdout, then print the error to
+  stderr, and exit with code 1. Use this to understand what the
+  failing tactic was supposed to prove.
+
+Standard loader and prover options (`-I`, `-timeout`, `-p`, etc.) are
+also available.
+
+### Output conventions
+
+- **Goals** are printed to **stdout**.
+- **Errors** are printed to **stderr**.
+- **Exit code 0** means success (or `-upto` reached its target).
+- **Exit code 1** means a command failed.
+- If there is no active proof at the point where goals are requested,
+  stdout will contain: `No active proof.`
+
+### Workflow for writing and debugging proofs
+
+1. Try to write a pen-and-paper proof first.
+
+2. Write the `.ec` file with your proof attempt. For a large proof,
+   write down skeleton and `admit` subgoals first, and then detail
+   the proof.
+
+3. Run `easycrypt llm -lastgoals FILE.ec` to check the full file.
+   - If it succeeds (exit 0), you are done.
+   - If it fails (exit 1), read the error from stderr and the goal
+     state from stdout to understand what went wrong.
+
+4. Use `-upto LINE` to inspect the proof state at a specific point
+   without running the rest of the file. This is useful for
+   incremental proof development.
+
+5. Fix the proof and repeat from step 2. The ultimate proof should
+   not contain `admit` or `admitted`.
+
+## EasyCrypt language overview
+
+### File structure
+
+An EasyCrypt file typically begins with `require` and `import`
+statements, followed by type, operator, and module declarations, and
+then lemma statements with their proofs.
+
+```
+require import AllCore List.
+
+type key.
+op n : int.
+axiom gt0_n : 0 < n.
+
+lemma foo : 0 < n + 1.
+proof. smt(gt0_n). qed.
+```
+
+### Proofs
+
+A proof is delimited by `proof.` and `qed.`. Inside, tactics are
+applied sequentially to transform the goal until it is discharged.
+
+```
+lemma bar (x : int) : x + 0 = x.
+proof. by ring. qed.
+```
+
+### Common tactics
+
+<!-- TODO: expand this section with descriptions and examples -->
+
+- `trivial` — solve trivial goals
+- `smt` / `smt(lemmas...)` — call SMT solvers, optionally with hints
+- `auto` — automatic reasoning
+- `split` — split conjunctions
+- `left` / `right` — choose a disjunct
+- `assumption` — close goal from a hypothesis
+- `apply H` — apply a hypothesis or lemma
+- `rewrite H` — rewrite using an equality
+- `have : P` — introduce an intermediate goal
+- `elim` — elimination / induction
+- `case` — case analysis
+- `congr` — congruence
+- `ring` / `field` — algebraic reasoning
+- `proc` — unfold a procedure (program logics)
+- `inline` — inline a procedure call
+- `sp` / `wp` — symbolic execution (forward / backward)
+- `if` — handle conditionals in programs
+- `while I` — handle while loops with invariant `I`
+- `rnd` — handle random sampling
+- `seq N : P` — split a program at statement `N` with mid-condition `P`
+- `conseq` — weaken/strengthen pre/postconditions
+- `byequiv` / `byphoare` — switch between program logics
+- `skip` — skip trivial program steps
+- `sim` — similarity (automatic relational reasoning)
+- `ecall` — external call
+
+### Tactic combinators
+
+- `by tac.` — apply `tac` and require all goals to be closed
+- `tac1; tac2` — sequence
+- `try tac` — try, ignore failure
+- `do tac` / `do N tac` — repeat
+- `[tac1 | tac2 | ...]` — apply different tactics to each subgoal
+- `tac => //.` — apply `tac`, then try `trivial` on generated subgoals
+- `move=> H` / `move=> /H` — introduction and views
+
+### Key libraries
+
+- `AllCore` — re-exports the core libraries (logic, integers, reals,
+  lists, etc.)
+- `Distr` — probability distributions
+- `DBool`, `DInterval`, `DList` — specific distributions
+- `FSet`, `FMap` — finite sets and maps
+- `SmtMap` — maps with SMT support
+- `PROM` — programmable/lazy random oracles
+
+### Guidelines
+
+* Use SMT solver only in direct mode (smt() or /#) on simple goals (arithmetic goals, pure logical goals).
+
+* Refrain from unfolding operator definitions unless necessary.
+  If you need more properties on an operator, state this property in a dedicated lemma,
+  but avoid unfolding definitions in higher level proofs.
+

src/ec.ml

@@ -415,6 +415,7 @@ let main () =
       (*---*) gccompact   : int option;
       (*---*) docgen      : bool;
       (*---*) outdirp     : string option;
+      (*---*) upto        : (int * int option) option;
       mutable trace       : trace1 list option;
     }
 
@@ -493,6 +494,7 @@ let main () =
         ; gccompact   = None
         ; docgen      = false
         ; outdirp     = None
+        ; upto        = None
         ; trace       = None }
 
     end
@@ -528,10 +530,40 @@ let main () =
         ; gccompact   = cmpopts.cmpo_compact
         ; docgen      = false
         ; outdirp     = None
+        ; upto        = None
         ; trace       = trace0 }
 
       end
 
+    | `Llm llmopts -> begin
+        let name = llmopts.llmo_input in
+
+        begin try
+          let ext = Filename.extension name in
+          ignore (EcLoader.getkind ext : EcLoader.kind)
+        with EcLoader.BadExtension ext ->
+          Format.eprintf "do not know what to do with %s@." ext;
+          exit 1
+        end;
+
+        let lastgoals = llmopts.llmo_lastgoals in
+        let terminal =
+          lazy (T.from_channel ~name ~progress:`Silent ~lastgoals (open_in name))
+        in
+
+        { prvopts     = {llmopts.llmo_provers with prvo_iterate = true}
+        ; input       = Some name
+        ; terminal    = terminal
+        ; interactive = false
+        ; eco         = true
+        ; gccompact   = None
+        ; docgen      = false
+        ; outdirp     = None
+        ; upto        = llmopts.llmo_upto
+        ; trace       = None }
+
+      end
+
     | `Runtest _ ->
         (* Eagerly executed *)
         assert false
@@ -572,6 +604,7 @@ let main () =
         ; gccompact   = None
         ; docgen      = true
         ; outdirp     = docopts.doco_outdirp
+        ; upto        = None
         ; trace       = None }
       end
 
@@ -585,7 +618,7 @@ let main () =
        | Some pwd -> EcCommands.addidir pwd);
 
   (* Check if the .eco is up-to-date and exit if so *)
-  (if not state.docgen then
+  (if not state.docgen && state.upto = None then
     oiter
       (fun input -> if EcCommands.check_eco input then exit 0)
       state.input);
@@ -669,6 +702,16 @@ let main () =
   if T.interactive terminal then
     T.notice ~immediate:true `Warning copyright terminal;
 
+  (* Check if a location is past the -upto point *)
+  let past_upto (loc : EcLocation.t) =
+    match state.upto with
+    | None -> false
+    | Some (line, col) ->
+        let (sl, sc) = loc.loc_start in
+        sl > line || (sl = line && match col with
+          | None -> true
+          | Some c -> sc >= c) in
+
   try
     if T.interactive terminal then Sys.catch_break true;
 
@@ -737,6 +780,14 @@ let main () =
               List.iter
                 (fun p ->
                    let loc = p.EP.gl_action.EcLocation.pl_loc in
+
+                   (* -upto: if this command starts past the target, print goals and exit *)
+                   if past_upto loc then begin
+                     T.finalize terminal;
+                     EcCommands.pp_current_goal_or_noproof ~all:true Format.std_formatter;
+                     exit 0
+                   end;
+
                    let timed = p.EP.gl_debug = Some `Timed in
                    let break = p.EP.gl_debug = Some `Break in
                    let ignore_fail = ref false in

src/ecCommands.ml

@@ -1024,6 +1024,13 @@ let pp_current_goal ?(all = false) stream =
       end
   end
 
+(* -------------------------------------------------------------------- *)
+let pp_current_goal_or_noproof ?(all = false) stream =
+  if Option.is_some (S.xgoal (current ())) then
+    pp_current_goal ~all stream
+  else
+    Format.fprintf stream "No active proof.@\n%!"
+
 (* -------------------------------------------------------------------- *)
 let pp_maybe_current_goal stream =
   match (Pragma.get ()).pm_verbose with

src/ecCommands.mli

@@ -60,6 +60,7 @@ val doc_comment : [`Global | `Item] * string -> unit
 
 (* -------------------------------------------------------------------- *)
 val pp_current_goal : ?all:bool -> Format.formatter -> unit
+val pp_current_goal_or_noproof : ?all:bool -> Format.formatter -> unit
 val pp_maybe_current_goal : Format.formatter -> unit
 val pp_all_goals : unit -> string list
 

src/ecOptions.ml

@@ -10,6 +10,7 @@ type command = [
   | `Runtest of run_option
   | `Why3Config
   | `DocGen of doc_option
+  | `Llm of llm_option
 ]
 
 and options = {
@@ -47,6 +48,13 @@ and doc_option = {
   doco_outdirp   : string option;
 }
 
+and llm_option = {
+  llmo_input     : string;
+  llmo_provers   : prv_options;
+  llmo_lastgoals : bool;
+  llmo_upto      : (int * int option) option;
+}
+
 and prv_options = {
   prvo_maxjobs    : int option;
   prvo_timeout    : int option;
@@ -351,6 +359,12 @@ let specs = {
       `Spec  ("trace"  , `Flag  , "Save all goals & messages in .eco");
       `Spec  ("compact", `Int   , "<internal>")]);
 
+    ("llm", "LLM-friendly batch compilation", [
+      `Group "loader";
+      `Group "provers";
+      `Spec  ("lastgoals" , `Flag  , "Print last unproved goals on failure");
+      `Spec  ("upto"      , `String, "Compile up to LINE or LINE:COL and print goals")]);
+
     ("cli", "Run EasyCrypt top-level", [
       `Group "loader";
       `Group "provers";
@@ -533,6 +547,27 @@ let doc_options_of_values values input =
   { doco_input     = input;
     doco_outdirp   = get_string "outdir" values; }
 
+let parse_upto values =
+  get_string "upto" values |> Option.map (fun s ->
+    let invalid () =
+      raise (Arg.Bad (Printf.sprintf
+        "invalid -upto format: expected LINE or LINE:COL, got %S" s)) in
+    match String.split_on_char ':' s with
+    | [line] ->
+        let line = try int_of_string line with Failure _ -> invalid () in
+        (line, None)
+    | [line; col] ->
+        let line = try int_of_string line with Failure _ -> invalid () in
+        let col  = try int_of_string col  with Failure _ -> invalid () in
+        (line, Some col)
+    | _ -> invalid ())
+
+let llm_options_of_values ini values input =
+  { llmo_input     = input;
+    llmo_provers   = prv_options_of_values ini values;
+    llmo_lastgoals = get_flag "lastgoals" values;
+    llmo_upto      = parse_upto values; }
+
 (* -------------------------------------------------------------------- *)
 let parse getini argv =
   let (command, values, anons) = parse specs argv in
@@ -604,6 +639,17 @@ let parse getini argv =
           raise (Arg.Bad "this command takes a single input file as argument")
       end
 
+    | "llm" -> begin
+        match anons with
+        | [input] ->
+           let ini = getini (Some input) in
+           let cmd = `Llm (llm_options_of_values ini values input) in
+           (cmd, ini, true)
+
+        | _ ->
+           raise (Arg.Bad "this command takes a single argument")
+      end
+
     | _ -> assert false
 
   in {

src/ecOptions.mli

@@ -6,6 +6,7 @@ type command = [
   | `Runtest of run_option
   | `Why3Config
   | `DocGen of doc_option
+  | `Llm of llm_option
 ]
 
 and options = {
@@ -43,6 +44,13 @@ and doc_option = {
   doco_outdirp   : string option;
 }
 
+and llm_option = {
+  llmo_input     : string;
+  llmo_provers   : prv_options;
+  llmo_lastgoals : bool;
+  llmo_upto      : (int * int option) option;
+}
+
 and prv_options = {
   prvo_maxjobs    : int option;
   prvo_timeout    : int option;