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

README.md

@@ -26,7 +26,6 @@ EasyCrypt is part of the [Formosa Crypto project](https://formosa-crypto.org/).
     - [Visual Studio Code](#visual-studio-code)
 - [Useful Resources](#useful-resources)
   - [Examples](#examples)
-  - [LaTeX Formatting](#latex-formatting)
 
 # Installation
 
@@ -186,10 +185,3 @@ Examples of how to use EasyCrypt are in the `examples` directory. You
 will find basic examples at the root of this directory, as well as a
 more advanced example in the `MEE-CBC` sub-directory and a tutorial on
 how to use the complexity system in `cost` sub-directory.
-
-## LaTeX Formatting
-
-LaTeX style file is in `assets/latex` directory. The basic usages are
-`\begin{eclst} ... \end{eclst}` (display mode) and
-`\ecinl{proc main() = { ...  }}` (inline mode).
-

assets/latex/eclistings.sty

@@ -254,8 +254,8 @@ let process_unroll_for ~cfold side cpos tc =
         e
 
     | _ -> tc_error !!tc
-             "last instruction of the while loop must be \
-              an \"increment\" of the loop counter" in
+             "last instruction of the while loop must be"
+             "an \"increment\" of the loop counter" in
 
   (* Apply loop increment *)
   let incrz =

src/phl/ecPhlLoopTx.ml

@@ -3,13 +3,19 @@ require import AllCore List IntDiv Binomial Ring StdOrder.
 (*---*) import IntID IntOrder.
 
 (* -------------------------------------------------------------------- *)
-op allperms_r (n : unit list) (s : 'a list) : 'a list list =
-with n = [] => [[]]
-with n = x::n => flatten (
+op allperms_r (n : unit list) (s : 'a list) : 'a list list.
+
+axiom allperms_r0 (s : 'a list) :
+  allperms_r [] s = [[]].
+
+axiom allperms_rS (x : unit) (n : unit list) (s : 'a list) :
+  allperms_r (x :: n) s = flatten (
     map (fun x => map ((::) x) (allperms_r n (rem x s))) (undup s)).
 
 op allperms (s : 'a list) = allperms_r (nseq (size s) tt) s.
 
+hint rewrite ap_r : allperms_r0 allperms_rS.
+
 (* -------------------------------------------------------------------- *)
 lemma allperms_rP n (s t : 'a list) : size s = size n =>
   (mem (allperms_r n s) t) <=> (perm_eq s t).
@@ -45,7 +51,7 @@ qed.
 (* -------------------------------------------------------------------- *)
 lemma uniq_allperms_r n (s : 'a list) : uniq (allperms_r n s).
 proof.
-elim: n s => [|? n ih] s; rewrite ?ap_r  //=.
+elim: n s => [|? n ih] s; rewrite ?ap_r  //.
 apply/uniq_flatten_map/undup_uniq.
   by move=> x /=; apply/map_inj_in_uniq/ih => a b _ _ [].
 move=> x y; rewrite !mem_undup => sx sy /= /hasP[t].
@@ -73,7 +79,7 @@ require import StdBigop.
 lemma size_allperms_uniq_r n (s : 'a list) : size s = size n => uniq s =>
   size (allperms_r n s) = fact (size s).
 proof.
-elim: n s => /= [s|n ih s].
+elim: n s => /= [|? n ih] s; rewrite ?ap_r /=.
   by move/size_eq0=> -> /=; rewrite fact0.
 case: s=> [|x s]; first by rewrite addz_neq0 ?size_ge0.
 (pose s' := undup _)=> /=; move/addrI=> eq_sz [Nsz uqs].