diff --git a/README.md b/README.md index 9ef3d2917e..902d7bc3cb 100644 --- a/README.md +++ b/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). - diff --git a/assets/latex/eclistings.sty b/assets/latex/eclistings.sty deleted file mode 100644 index 7b5c15d681..0000000000 --- a/assets/latex/eclistings.sty +++ /dev/null @@ -1,155 +0,0 @@ -\NeedsTeXFormat{LaTeX2e} -\ProvidesPackage{eclistings}[2026/04/07 EasyCrypt listings] - -\RequirePackage{listings} -\RequirePackage{xcolor} -\RequirePackage{xparse} - -% EasyCrypt % Language -\lstdefinelanguage{easycrypt}{% - sensitive=true, % Case sensitive keywords - % Keywords: Global and programming language - morekeywords=[1]% - { - Pr, Self, Top, abbrev, abort, abstract, as, axiom, axiomatized, clone, const, - declare, dump, end, exception, exit, export, from, global, goal, hint, import, - include, inductive, instance, lemma, local, locate, module, notation, of, op, - pred, print, proof, prover, qed, realize, remove, rename, require, search, - section, subtype, theory, timeout, type, why3, with, - async, ehoare, elif, else, equiv, exists, for, forall, fun, glob, hoare, if, - in, is, islossless, let, match, phoare, proc, raise, res, return, then, var, - while - }, - % Keywords: Regular (i.e., non-closing) tactics - morekeywords=[2]% - { - algebra, alias, apply, auto, beta, byehoare, byequiv, byphoare, bypr, byupto, - call, case, cbv, cfold, change, clear, congr, conseq, delta, eager, ecall, - elim, eta, exfalso, exlim, fel, field, fieldeq, fission, fusion, gen, have, - idassign, idtac, inline, interleave, iota, kill, left, logic, modpath, move, - outline, pose, pr_bounded, progress, rcondf, rcondt, replace, rewrite, right, - ring, ringeq, rnd, rndsem, rwnormal, seq, sim, simplify, skip, sp, split, - splitwhile, subst, suff, swap, symmetry, transitivity, trivial, unroll, - weakmem, wlog, wp, zeta - }, - % Keywords: Closing/byclose tactics and dangerous commands - morekeywords=[3]% - { - admit, admitted, - assumption, by, check, coq, done, edit, exact, fix, reflexivity, smt, solve - }, - % Keywords: Tacticals and internal - morekeywords=[4]% - { - do, expect, first, last, try, - debug, fail, pragma, time, undo - }, - comment=[n]{(*}{*)}, % Multi-line, nested comments delimited by (* and *) - string=[d]{"}, % Strings delimited by " and ", non-escapable -} - -% Style (base/default) -\lstdefinestyle{easycrypt-base}{% - % Frame - captionpos=t, % Position caption at top (mirroring what's typical for algorithms) - frame=tb, % Top and bottom rules - framesep=\smallskipamount, % Small skip between frame and listing content - % Float placement - floatplacement=tbhp, - % Character printing and placement - upquote=true, % Print backtick and single quote as is - columns=[c]fixed, % Monospace characters, centered in their box - keepspaces=true, % Don't drop spaces for column alignment - tabsize=2, % Tabstops every 2 spaces - mathescape=false, % Don't allow escaping to LaTeX with $ - showstringspaces=false, % Don't print characters for spaces - % Line numbers - numbers=none, % No line numbers - % Basic style - basicstyle={\normalsize\ttfamily}, - % Style for (non-keyword) identifiers - identifierstyle={}, -} - -% Define default colors based on availability of colorblind colors -\@ifpackageloaded{colorblind}{ - \lstdefinestyle{easycrypt-default}{% - style=easycrypt-base, - % Styles for different keyword classes - keywordstyle=[1]{\color{T-Q-B6}},% - keywordstyle=[2]{\color{T-Q-B1}},% - keywordstyle=[3]{\color{T-Q-B5}},% - keywordstyle=[4]{\color{T-Q-B4}},% - % Styles for comments and strings - commentstyle={\itshape\color{T-Q-B0}},% - stringstyle={\color{T-Q-B3}}, - % Style of line numbers (in case numbers is overwritten to true) - numberstyle={\small\color{T-Q-B0}}, - } -}{% - \lstdefinestyle{easycrypt-default}{% - style=easycrypt-base, - % Styles for different keyword classes - keywordstyle=[1]{\color{violet}},% - keywordstyle=[2]{\color{blue}},% - keywordstyle=[3]{\color{red}},% - keywordstyle=[4]{\color{olive}},% - % Styles for comments and strings - commentstyle={\itshape\color{gray}},% - stringstyle={\color{green}}, - % Style of line numbers (in case numbers is overwritten to true) - numberstyle={\small\color{gray}}, - } -} - -% Style for drafting/debugging (explicit spaces/tabs) -\lstdefinestyle{easycrypt-draft}{% - style=easycrypt-default, - showspaces=true, - showtabs=true, - showstringspaces=true, -} - -% Style without top/bottom frame rules -\lstdefinestyle{easycrypt-plain}{% - style=easycrypt-default, - frame=none, - framesep=0pt, - basicstyle={\small\ttfamily}, - aboveskip=0.3\baselineskip, - belowskip=0.3\baselineskip, - columns=fullflexible -} - -% Environments % Default, non-floating environment % Meant to be used inside -%other (potentially floating) environment % that takes care of the caption and -%surrounding spacing -\lstnewenvironment{eclst}[1][]{% - \lstset{% - language=easycrypt,% - style=easycrypt-default,% - aboveskip=\smallskipamount,% Equal to framesep of style if top rule, else 0pt - belowskip=\smallskipamount,% Equal to framesep of style if bottom rule, else 0pt - abovecaptionskip=0pt,% - belowcaptionskip=0pt,% - #1% - }% -}{} - -% Inline -\NewDocumentCommand{\ecinl}{O{easycrypt-default} m O{}}{% - \lstinline[% - language=easycrypt,% - style=#1,% - breaklines,% - breakindent=0pt,% - columns=fullflexible,% - #3% - ]{#2}% -} - -\NewDocumentCommand{\ecinlfoot}{O{easycrypt-default} m O{}}{% - \ecinl[#1]{#2}[basicstyle={\footnotesize\ttfamily},#3]% -} - -\endinput \ No newline at end of file diff --git a/doc/llm/CLAUDE.md b/doc/llm/CLAUDE.md new file mode 100644 index 0000000000..0cc20c5a38 --- /dev/null +++ b/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 + + + +- `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. + diff --git a/src/ec.ml b/src/ec.ml index 627d25b81b..ada7602b58 100644 --- a/src/ec.ml +++ b/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 diff --git a/src/ecCommands.ml b/src/ecCommands.ml index 438295196e..474eab8888 100644 --- a/src/ecCommands.ml +++ b/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 diff --git a/src/ecCommands.mli b/src/ecCommands.mli index a72d31a437..e411b99d6c 100644 --- a/src/ecCommands.mli +++ b/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 diff --git a/src/ecOptions.ml b/src/ecOptions.ml index f012e8e8d6..52a4d6e66b 100644 --- a/src/ecOptions.ml +++ b/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 , "")]); + ("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 { diff --git a/src/ecOptions.mli b/src/ecOptions.mli index 59009718ad..7ac81ec0a4 100644 --- a/src/ecOptions.mli +++ b/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; diff --git a/src/ecTerminal.ml b/src/ecTerminal.ml index 94f7c048e5..c5f85bc814 100644 --- a/src/ecTerminal.ml +++ b/src/ecTerminal.ml @@ -148,8 +148,9 @@ type progress = [ `Human | `Script | `Silent ] class from_channel ?(gcstats : bool = true) ?(progress : progress option) - ~(name : string) - (stream : in_channel) + ?(lastgoals : bool = false) + ~(name : string) + (stream : in_channel) : terminal = object(self) @@ -260,11 +261,11 @@ class from_channel self#_clean_progress_line (); begin match progress with | `Human -> - Format.eprintf "[%s] [%s] %s\n%!" prefix strloc msg; + Format.eprintf "[%s] [%s] %s\n%!" prefix strloc msg | `Script -> Format.eprintf "E %s %s %s\n%!" prefix strloc (String.escaped msg) | `Silent -> - () + Format.eprintf "[%s] [%s] %s\n%!" prefix strloc msg end; self#_update_progress @@ -290,6 +291,8 @@ class from_channel let msg = String.strip (EcPException.tostring e) in self#_clean_progress_line (); + if lastgoals then + EcCommands.pp_current_goal_or_noproof ~all:true Format.std_formatter; self#_notice ?subloc ~immediate:true `Critical msg; self#_update_progress; self#_clean_progress_line ~erase:false (); @@ -314,5 +317,5 @@ class from_channel Format.pp_set_margin Format.err_formatter i end -let from_channel ?gcstats ?progress ~name stream = - new from_channel ?gcstats ?progress ~name stream +let from_channel ?gcstats ?progress ?lastgoals ~name stream = + new from_channel ?gcstats ?progress ?lastgoals ~name stream diff --git a/src/ecTerminal.mli b/src/ecTerminal.mli index 0a96a56d24..faacff0e7f 100644 --- a/src/ecTerminal.mli +++ b/src/ecTerminal.mli @@ -22,6 +22,7 @@ type progress = [ `Human | `Script | `Silent ] val from_channel : ?gcstats:bool -> ?progress:progress + -> ?lastgoals:bool -> name:string -> in_channel -> terminal diff --git a/src/phl/ecPhlLoopTx.ml b/src/phl/ecPhlLoopTx.ml index 71f33072dc..b8bf396d5e 100644 --- a/src/phl/ecPhlLoopTx.ml +++ b/src/phl/ecPhlLoopTx.ml @@ -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 = diff --git a/theories/algebra/Perms.ec b/theories/algebra/Perms.ec index 1ebc0e1d70..5423d79128 100644 --- a/theories/algebra/Perms.ec +++ b/theories/algebra/Perms.ec @@ -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].