From fe9fba3e9e725ee6ab579847e8988f2c35e2b100 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sat, 11 Apr 2026 09:12:50 +0200 Subject: [PATCH 1/2] Add goal printing flags (-upto, -lastgoals) and LLM agent guide Add two new flags for the `easycrypt` CLI to support LLM coding agents: - `-upto `: 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. --- README.md | 8 -- assets/latex/eclistings.sty | 155 ------------------------------------ doc/llm/CLAUDE.md | 149 ++++++++++++++++++++++++++++++++++ src/ec.ml | 53 +++++++++++- src/ecCommands.ml | 7 ++ src/ecCommands.mli | 1 + src/ecOptions.ml | 46 +++++++++++ src/ecOptions.mli | 8 ++ src/ecTerminal.ml | 15 ++-- src/ecTerminal.mli | 1 + src/phl/ecPhlLoopTx.ml | 4 +- theories/algebra/Perms.ec | 16 ++-- 12 files changed, 286 insertions(+), 177 deletions(-) delete mode 100644 assets/latex/eclistings.sty create mode 100644 doc/llm/CLAUDE.md 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]. From 7e5a8c47c4c57b3c14df99600ee8ac1480ea55c4 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Sun, 12 Apr 2026 23:31:51 +0200 Subject: [PATCH 2/2] Add tentative auto-generated EasyCrypt language documentation This is a first draft covering: types, operators, predicates, expressions, formulas, programs, modules, module types, theories, sections, cloning, hints, printing, and standard library tour. --- doc/index.rst | 1 + doc/language.rst | 8 + doc/language/01-overview.rst | 160 ++++++++++++ doc/language/02-types.rst | 297 ++++++++++++++++++++++ doc/language/03-operators.rst | 254 +++++++++++++++++++ doc/language/04-expressions.rst | 384 +++++++++++++++++++++++++++++ doc/language/05-formulas.rst | 239 ++++++++++++++++++ doc/language/06-programs.rst | 281 +++++++++++++++++++++ doc/language/07-modules.rst | 250 +++++++++++++++++++ doc/language/08-theories.rst | 266 ++++++++++++++++++++ doc/language/09-cloning.rst | 274 ++++++++++++++++++++ doc/language/10-hints-printing.rst | 195 +++++++++++++++ doc/language/11-stdlib.rst | 361 +++++++++++++++++++++++++++ 13 files changed, 2970 insertions(+) create mode 100644 doc/language.rst create mode 100644 doc/language/01-overview.rst create mode 100644 doc/language/02-types.rst create mode 100644 doc/language/03-operators.rst create mode 100644 doc/language/04-expressions.rst create mode 100644 doc/language/05-formulas.rst create mode 100644 doc/language/06-programs.rst create mode 100644 doc/language/07-modules.rst create mode 100644 doc/language/08-theories.rst create mode 100644 doc/language/09-cloning.rst create mode 100644 doc/language/10-hints-printing.rst create mode 100644 doc/language/11-stdlib.rst diff --git a/doc/index.rst b/doc/index.rst index 8b6c7d9b2f..397407b4f4 100644 --- a/doc/index.rst +++ b/doc/index.rst @@ -4,4 +4,5 @@ EasyCrypt reference manual .. toctree:: :maxdepth: 2 + language tactics diff --git a/doc/language.rst b/doc/language.rst new file mode 100644 index 0000000000..ae9e4e7cfd --- /dev/null +++ b/doc/language.rst @@ -0,0 +1,8 @@ +The EasyCrypt language +======================================================================== + +.. toctree:: + :maxdepth: 1 + :glob: + + language/* diff --git a/doc/language/01-overview.rst b/doc/language/01-overview.rst new file mode 100644 index 0000000000..3974ffc7f4 --- /dev/null +++ b/doc/language/01-overview.rst @@ -0,0 +1,160 @@ +.. _language-overview: + +======================================================================== +Overview +======================================================================== + +EasyCrypt is an interactive proof assistant designed for reasoning about +the security of cryptographic constructions. It provides: + +- A **typed functional language** for writing mathematical definitions: + types, operators, predicates, lemmas, and proofs. + +- An **imperative programming language** for describing the behavior + of cryptographic algorithms and adversaries as probabilistic programs. + +- A collection of **program logics** -- Hoare logic, probabilistic + Hoare logic, probabilistic relational Hoare logic, and others -- for + reasoning about the behavior of those programs. + +This chapter introduces the general structure of EasyCrypt files and +how the various pieces fit together. + +.. contents:: + :local: + +------------------------------------------------------------------------ +File structure +------------------------------------------------------------------------ + +An EasyCrypt source file has the extension ``.ec``. A file consists of +a sequence of top-level declarations and definitions. The main kinds +of top-level items are: + +- **Type declarations**: introduce new types (abstract, aliases, + records, algebraic datatypes). + +- **Operator and predicate declarations**: introduce new functions and + predicates, either abstract or with a concrete definition. + +- **Axioms and lemmas**: state properties (axioms are assumed, lemmas + must be proved). + +- **Module type declarations**: describe the interface of a module + (a collection of mutable state and procedures). + +- **Module declarations**: define modules that implement a module type. + +- **Theories**: group related declarations together under a name. + +- **Sections**: provide a scoping mechanism for local assumptions. + +- **Clone directives**: instantiate abstract theories with concrete + definitions. + +Items are terminated by a period (``.``). + +Here is a minimal EasyCrypt file that declares a type, defines an +operator, and states a lemma: + +.. code-block:: easycrypt + + require import AllCore. + + type color = [Red | Green | Blue]. + + op is_primary (c : color) : bool = + with c = Red => true + with c = Green => false + with c = Blue => true. + + lemma red_is_primary : is_primary Red. + proof. by []. qed. + +------------------------------------------------------------------------ +Loading theories +------------------------------------------------------------------------ + +EasyCrypt files can load other files (called *theories*) using the +``require`` command: + +.. code-block:: easycrypt + + require AllCore. + +This makes the contents of ``AllCore`` available under a qualified +name (e.g. ``AllCore.List.size``). To bring the names into scope +without qualification, add ``import``: + +.. code-block:: easycrypt + + require import AllCore. + +There is also ``export``, which re-exports the imported names so that +any file that later imports the current file also sees them: + +.. code-block:: easycrypt + + require export AllCore. + +You can require several theories at once: + +.. code-block:: easycrypt + + require import AllCore List FSet. + +The ``import`` and ``export`` keywords can also be used standalone to +import or export a theory that has already been required: + +.. code-block:: easycrypt + + require AllCore. + import AllCore. + +------------------------------------------------------------------------ +Comments +------------------------------------------------------------------------ + +Comments in EasyCrypt are delimited by ``(*`` and ``*)`` and can be +nested: + +.. code-block:: easycrypt + + (* This is a comment *) + + (* Comments (* can be *) nested *) + +------------------------------------------------------------------------ +A first example +------------------------------------------------------------------------ + +To give a flavor of how the language pieces fit together, here is a +small but complete example. It defines an abstract type, an operator +over that type, and proves a simple property. + +.. code-block:: easycrypt + + require import AllCore. + + (* An abstract type with decidable equality *) + type key. + + (* A simple operator *) + op xor (x y : key) : key. + + (* We assume xor is involutive *) + axiom xorK (x y : key) : xor (xor x y) y = x. + + (* A consequence: xor is a left-inverse of itself *) + lemma xor_cancel (x y : key) : xor (xor x y) y = x. + proof. by apply xorK. qed. + +The following chapters describe each part of the language in detail. +:ref:`Types ` covers the type system. +:ref:`Operators and predicates ` explains how to +define functions and predicates. :ref:`Expressions ` +and :ref:`Formulas ` describe the term language. +:ref:`Programs ` introduces the imperative fragment. +:ref:`Modules ` covers the module system. +:ref:`Theories and sections ` and +:ref:`Cloning ` explain theory management. diff --git a/doc/language/02-types.rst b/doc/language/02-types.rst new file mode 100644 index 0000000000..4cd1206d17 --- /dev/null +++ b/doc/language/02-types.rst @@ -0,0 +1,297 @@ +.. _language-types: + +======================================================================== +Types +======================================================================== + +Every expression in EasyCrypt has a type. Types classify values: +integers, booleans, lists, functions, distributions, and so on. This +chapter describes the type system, starting with the built-in types +and working up to user-defined types. + +.. contents:: + :local: + +------------------------------------------------------------------------ +Built-in types +------------------------------------------------------------------------ + +EasyCrypt provides the following primitive types. They are always in +scope (defined in the ``Pervasive`` prelude). + +``unit`` + The unit type. It has a single value, written ``tt``. It is used + when no meaningful value needs to be returned. + +``bool`` + The type of booleans, with values ``true`` and ``false``. + +``int`` + The type of (unbounded) integers. Integer literals are written as + usual: ``0``, ``42``, ``-3``. Hexadecimal literals are also + supported: ``0x1A2B``. + +``real`` + The type of real numbers. Real literals are written with a decimal + point or as a ratio: ``0.5``, ``3.14``, ``1%r`` (the integer 1 + coerced to a real). + +``'a distr`` + The type of (sub-)distributions over a type ``'a``. A value of + type ``'a distr`` assigns a probability (a non-negative real) to + each value of type ``'a``, with the total probability at most 1. + +``'a option`` + The option type, with constructors ``None`` and ``Some``. It is + defined in the ``Logic`` prelude as an algebraic datatype. + +``exn`` + The type of exceptions. New exception constructors are introduced + by ``exception`` declarations (see :ref:`language-programs`). + +All types in EasyCrypt are *inhabited*: there is a polymorphic +constant ``witness : 'a`` that provides a default value for any type. +This means there is no empty type. + +------------------------------------------------------------------------ +Type variables and polymorphism +------------------------------------------------------------------------ + +Types can be parameterized by *type variables*, which are written with +a leading tick: ``'a``, ``'b``, ``'key``, etc. Polymorphic +definitions work for any choice of type arguments. + +For example, the identity function is polymorphic in its argument type: + +.. code-block:: easycrypt + + op id (x : 'a) : 'a = x. + +When using a polymorphic operator, EasyCrypt infers the type arguments +automatically in most cases. When it cannot, you can supply them +explicitly using angle-bracket syntax: + +.. code-block:: easycrypt + + op id<:int> 42. + +------------------------------------------------------------------------ +Tuples +------------------------------------------------------------------------ + +Given types ``t1``, ``t2``, ..., ``tn``, the product type +``t1 * t2 * ... * tn`` is the type of tuples of those types. Tuple +values are written with parentheses and commas: + +.. code-block:: easycrypt + + (1, true) (* : int * bool *) + (1, true, 42) (* : int * bool * int *) + +Tuple components are accessed by *projection*, written with a +backtick and a 1-based index: + +.. code-block:: easycrypt + + op fst_example : int = (1, true).`1. (* = 1 *) + op snd_example : bool = (1, true).`2. (* = true *) + +The standard library also provides ``fst`` and ``snd`` abbreviations +for pairs. + +Pattern matching on tuples is supported in ``let`` bindings and in +operator definitions: + +.. code-block:: easycrypt + + op swap (p : 'a * 'b) : 'b * 'a = + let (x, y) = p in (y, x). + +------------------------------------------------------------------------ +Function types +------------------------------------------------------------------------ + +The type ``t1 -> t2`` is the type of functions from ``t1`` to ``t2``. +Function types associate to the right: + +.. code-block:: easycrypt + + (* These are the same type: *) + (* int -> int -> bool *) + (* int -> (int -> bool) *) + +Functions are first-class values. You can pass them as arguments, +return them from operators, and store them in data structures. + +.. code-block:: easycrypt + + op apply (f : 'a -> 'b) (x : 'a) : 'b = f x. + + op compose (g : 'b -> 'c) (f : 'a -> 'b) : 'a -> 'c = + fun x => g (f x). + +------------------------------------------------------------------------ +Type declarations +------------------------------------------------------------------------ + +New types are introduced with the ``type`` keyword. There are several +forms. + +Abstract types +~~~~~~~~~~~~~~ + +An abstract type declaration introduces a type name with no definition. +Nothing is known about the type except that it is inhabited (it has a +``witness``). + +.. code-block:: easycrypt + + type key. + type 'a container. + +Abstract types are useful for specifying interfaces: you work with +the type name without committing to a representation. + +Type aliases +~~~~~~~~~~~~ + +A type alias gives a new name to an existing type expression: + +.. code-block:: easycrypt + + type point = int * int. + type 'a predicate = 'a -> bool. + +Aliases are transparent: ``point`` and ``int * int`` are +interchangeable everywhere. + +------------------------------------------------------------------------ +Record types +------------------------------------------------------------------------ + +A record type groups named fields together: + +.. code-block:: easycrypt + + type person = { + name : string; + age : int; + }. + +Record values are constructed with braces: + +.. code-block:: easycrypt + + op alice : person = {| name = "Alice"; age = 30; |}. + +Fields are accessed with dot notation: + +.. code-block:: easycrypt + + op alice_age : int = alice.`age. + +Records can also be updated functionally: + +.. code-block:: easycrypt + + op older_alice : person = {| alice with age = 31; |}. + +------------------------------------------------------------------------ +Algebraic datatypes +------------------------------------------------------------------------ + +An algebraic datatype (also called a *variant* or *sum type*) defines +a type by listing its constructors. Each constructor can carry zero +or more arguments. + +.. code-block:: easycrypt + + type color = [Red | Green | Blue]. + + type 'a tree = [ + | Leaf + | Node of 'a & 'a tree & 'a tree + ]. + +Constructors are introduced inside square brackets, separated by +``|``. Arguments of a constructor are separated by ``&`` (not ``*``, +which would denote a single tuple argument). + +Values of an algebraic datatype are built by applying a constructor: + +.. code-block:: easycrypt + + op example_tree : int tree = + Node 1 (Node 2 Leaf Leaf) Leaf. + +Pattern matching is the primary way to inspect algebraic datatypes. +See :ref:`language-expressions` for the ``match`` expression and +pattern-matching operator definitions. + +The ``option`` type is a standard algebraic datatype: + +.. code-block:: easycrypt + + type 'a option = [None | Some of 'a]. + +------------------------------------------------------------------------ +Subtypes +------------------------------------------------------------------------ + +A *subtype* carves out a subset of an existing type that satisfies +a predicate. The syntax is: + +.. code-block:: easycrypt + + subtype name = { x : carrier | predicate }. + +For example, to define a type of natural numbers as non-negative +integers: + +.. code-block:: easycrypt + + subtype nat = { x : int | 0 <= x }. + +A subtype declaration generates: + +- An injection from the subtype into the carrier type. +- A partial projection from the carrier type to the subtype (which + requires the predicate to hold). +- An axiom stating that the injection is indeed injective. +- An axiom stating that the projection is a left-inverse of the + injection on values satisfying the predicate. + +You can optionally provide a constructor name with ``as``: + +.. code-block:: easycrypt + + subtype nat AS Nat = { x : int | 0 <= x }. + +------------------------------------------------------------------------ +Type classes and instances +------------------------------------------------------------------------ + +EasyCrypt has a lightweight type-class mechanism, mainly used for +algebraic structures. The standard library defines type classes such +as ``ring`` and ``field``, along with associated operators and axioms. + +To declare that a type is an instance of a type class, use the +``instance`` keyword. For example, declaring that ``int`` is a +commutative ring: + +.. code-block:: easycrypt + + instance ring with int + op rzero = 0 + op rone = 1 + op radd = Int.(+) + op rmul = Int.( * ) + op ropp = Int.([-]) + proof. (* ... prove the ring axioms ... *) qed. + +Once an instance is registered, the ``ring`` and ``field`` proof +tactics can automatically solve equations over that type. + +Type classes are not something most users need to define; the standard +library provides the main ones. Understanding how to declare +*instances* is the important part. diff --git a/doc/language/03-operators.rst b/doc/language/03-operators.rst new file mode 100644 index 0000000000..407e0ae646 --- /dev/null +++ b/doc/language/03-operators.rst @@ -0,0 +1,254 @@ +.. _language-operators: + +======================================================================== +Operators and predicates +======================================================================== + +Operators and predicates are the building blocks of definitions in +EasyCrypt. An *operator* is a function that returns a value; a +*predicate* is a function that returns a boolean (a proposition). +This chapter explains how to declare and define them. + +.. contents:: + :local: + +------------------------------------------------------------------------ +Operator declarations +------------------------------------------------------------------------ + +Operators are introduced with the ``op`` keyword. + +Abstract operators +~~~~~~~~~~~~~~~~~~ + +An abstract operator has a name and a type but no definition: + +.. code-block:: easycrypt + + op f : int -> int. + op g : int -> int -> bool. + op h ['a] : 'a -> 'a -> bool. + +Nothing is known about an abstract operator except its type. Abstract +operators are useful inside abstract theories and sections, where +properties are stated as axioms and later instantiated. + +Concrete operators +~~~~~~~~~~~~~~~~~~ + +A concrete operator has a body. The simplest form takes arguments and +returns an expression: + +.. code-block:: easycrypt + + op double (x : int) : int = x + x. + op max (x y : int) : int = if x < y then y else x. + +The return type can often be inferred: + +.. code-block:: easycrypt + + op double (x : int) = x + x. + +Multiple arguments of the same type can share a type annotation: + +.. code-block:: easycrypt + + op add3 (x y z : int) = x + y + z. + +Pattern-matching definitions +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Operators over algebraic datatypes can be defined by pattern matching +using ``with`` clauses: + +.. code-block:: easycrypt + + type 'a option = [None | Some of 'a]. + + op odflt (d : 'a) (ox : 'a option) : 'a = + with ox = None => d + with ox = Some x => x. + + op omap (f : 'a -> 'b) (ox : 'a option) : 'b option = + with ox = None => None + with ox = Some x => Some (f x). + +The ``with`` clauses must be exhaustive: every constructor of the +datatype must appear. Nested patterns are supported. + +Operator aliases +~~~~~~~~~~~~~~~~ + +You can declare multiple names for the same operator in one declaration: + +.. code-block:: easycrypt + + op add, plus (x y : int) = x + y. + +Here both ``add`` and ``plus`` refer to the same operator. + +Polymorphic operators +~~~~~~~~~~~~~~~~~~~~~ + +Operators can be polymorphic. Type variables appearing in the arguments +or return type are universally quantified: + +.. code-block:: easycrypt + + op id (x : 'a) : 'a = x. + op const (x : 'a) (y : 'b) : 'a = x. + +You can also declare type variables explicitly using brackets: + +.. code-block:: easycrypt + + op id ['a] (x : 'a) : 'a = x. + +This is useful when a type variable appears only in the return type, +not in any argument. + +Operator symbols and infix notation +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Operators can be given symbolic names for use in infix, prefix, or +mixfix position. Symbolic operator names are enclosed in parentheses +in their declaration: + +.. code-block:: easycrypt + + op (+) (x y : int) : int. (* infix *) + op ([-]) (x : int) : int. (* prefix *) + +In expressions, these are used in their natural position: + +.. code-block:: easycrypt + + op example : int = 3 + 4. + op negation : int = -5. + +------------------------------------------------------------------------ +Predicate declarations +------------------------------------------------------------------------ + +A predicate is like an operator that returns ``bool``. The ``pred`` +keyword is a convenience for declaring such operators. + +Abstract predicates +~~~~~~~~~~~~~~~~~~~ + +.. code-block:: easycrypt + + pred P : int. (* P : int -> bool *) + pred R : int & int. (* R : int -> int -> bool *) + +Note: for predicates, multi-argument types are separated by ``&``, +not ``*`` or ``->``. + +Concrete predicates +~~~~~~~~~~~~~~~~~~~ + +.. code-block:: easycrypt + + pred is_positive (x : int) = 0 < x. + pred in_range (lo hi x : int) = lo <= x /\ x < hi. + +A ``pred`` definition is equivalent to an ``op`` definition with +return type ``bool``: + +.. code-block:: easycrypt + + (* These two are equivalent: *) + pred is_even (x : int) = x %% 2 = 0. + op is_even (x : int) : bool = x %% 2 = 0. + +------------------------------------------------------------------------ +Inductive predicates +------------------------------------------------------------------------ + +An *inductive predicate* defines a predicate as the smallest relation +closed under a set of rules. The syntax uses the ``inductive`` keyword: + +.. code-block:: easycrypt + + inductive is_even : int -> bool = + | Even0 : is_even 0 + | EvenSS (n : int) of is_even n : is_even (n + 2). + +Each constructor corresponds to an introduction rule. The declaration +generates: + +- The predicate itself. +- A constructor for each rule. +- An induction principle (elimination lemma). + +Inductive predicates are especially useful for defining reachability +relations, well-formedness conditions, and similar recursive +properties. + +------------------------------------------------------------------------ +Abbreviations +------------------------------------------------------------------------ + +An *abbreviation* (``abbrev``) defines an operator that is +automatically unfolded during type-checking and proof search. It is +essentially a macro: + +.. code-block:: easycrypt + + abbrev (<>) (x y : 'a) = !(x = y). + +Abbreviations are transparent -- they are expanded wherever they +appear. They can be useful for notational convenience. + +The ``[-printing]`` option prevents an abbreviation from being used +when EasyCrypt displays terms (so the expanded form is shown instead): + +.. code-block:: easycrypt + + abbrev [-printing] fst (p : 'a * 'b) : 'a = p.`1. + +With this option, EasyCrypt will display ``p.`1`` rather than +``fst p`` in goal output. + +------------------------------------------------------------------------ +Notations +------------------------------------------------------------------------ + +The ``notation`` command introduces syntactic sugar that is desugared +during parsing. Unlike abbreviations, notations can define arbitrary +mixfix syntax. + +.. code-block:: easycrypt + + notation myif <- <-b, 'a-> b x y : 'a = if b then x else y. + +Notations are an advanced feature primarily used in the standard +library. Most users do not need to define new notations. + +------------------------------------------------------------------------ +Locality +------------------------------------------------------------------------ + +Declarations can be prefixed with a *locality* modifier that controls +their visibility: + +``local`` + The declaration is visible only within the current theory. It is + not exported when the theory is required by another file. + + .. code-block:: easycrypt + + local op helper (x : int) = x + 1. + +``declare`` + The declaration is *abstract within a section* and is automatically + generalized when the section is closed. See + :ref:`language-theories` for details on sections. + + .. code-block:: easycrypt + + declare op f : int -> int. + +If no modifier is given, the declaration is *global*: it is visible +everywhere. diff --git a/doc/language/04-expressions.rst b/doc/language/04-expressions.rst new file mode 100644 index 0000000000..632f557264 --- /dev/null +++ b/doc/language/04-expressions.rst @@ -0,0 +1,384 @@ +.. _language-expressions: + +======================================================================== +Expressions +======================================================================== + +Expressions are the terms of the EasyCrypt logic. They denote values: +integers, booleans, functions, tuples, and so on. Expressions appear +in operator definitions, lemma statements, proof goals, and (in a +restricted form) inside programs. + +This chapter covers the syntax and meaning of expressions. The +distinction between expressions and *formulas* (which add logical +connectives and quantifiers) is discussed in :ref:`language-formulas`. + +.. contents:: + :local: + +------------------------------------------------------------------------ +Literals +------------------------------------------------------------------------ + +Integer literals +~~~~~~~~~~~~~~~~ + +Integer literals are written in decimal or hexadecimal: + +.. code-block:: easycrypt + + 42 + -3 + 0 + 0x1A2B + +Real literals +~~~~~~~~~~~~~ + +Real literals use a decimal point or the ``%r`` suffix to coerce an +integer to a real: + +.. code-block:: easycrypt + + 3.14 + 0.5 + 1%r (* the integer 1, coerced to real *) + +Boolean literals +~~~~~~~~~~~~~~~~ + +.. code-block:: easycrypt + + true + false + +The unit value +~~~~~~~~~~~~~~ + +The sole value of type ``unit`` is: + +.. code-block:: easycrypt + + tt + +------------------------------------------------------------------------ +Variables +------------------------------------------------------------------------ + +There are two kinds of variables in EasyCrypt. + +**Logical variables** appear in operator definitions, lemma statements, +and quantifiers. They are immutable and range over all values of their +type. Logical variables are simply written by name: + +.. code-block:: easycrypt + + x y key msg + +**Program variables** appear inside module procedures and in formulas +that refer to program state. They are discussed in +:ref:`language-programs` and :ref:`language-formulas`. + +------------------------------------------------------------------------ +Arithmetic and comparison operators +------------------------------------------------------------------------ + +The standard arithmetic operators are defined in the core libraries. +After ``require import AllCore``: + +.. list-table:: + :header-rows: 1 + :widths: 15 30 30 + + * - Operator + - Type + - Description + * - ``+`` + - ``int -> int -> int`` + - Addition + * - ``-`` + - ``int -> int -> int`` + - Subtraction + * - ``*`` + - ``int -> int -> int`` + - Multiplication + * - ``%%`` + - ``int -> int -> int`` + - Euclidean modulo (from ``IntDiv``) + * - ``%/`` + - ``int -> int -> int`` + - Euclidean division (from ``IntDiv``) + * - ``-`` (prefix) + - ``int -> int`` + - Negation + * - ``=`` + - ``'a -> 'a -> bool`` + - Equality (polymorphic) + * - ``<>`` + - ``'a -> 'a -> bool`` + - Disequality + * - ``<`` + - ``int -> int -> bool`` + - Strict less-than + * - ``<=`` + - ``int -> int -> bool`` + - Less-or-equal + * - ``>`` + - ``int -> int -> bool`` + - Strict greater-than + * - ``>=`` + - ``int -> int -> bool`` + - Greater-or-equal + +The same arithmetic operators are also available for ``real`` (after +importing the appropriate libraries). + +------------------------------------------------------------------------ +Boolean operators +------------------------------------------------------------------------ + +.. list-table:: + :header-rows: 1 + :widths: 15 30 30 + + * - Operator + - Type + - Description + * - ``!`` + - ``bool -> bool`` + - Negation (not) + * - ``/\`` + - ``bool -> bool -> bool`` + - Conjunction (and) + * - ``\/`` + - ``bool -> bool -> bool`` + - Disjunction (or) + * - ``=>`` + - ``bool -> bool -> bool`` + - Implication + * - ``<=>`` + - ``bool -> bool -> bool`` + - Equivalence (if and only if) + * - ``&&`` + - ``bool -> bool -> bool`` + - Short-circuit and + * - ``||`` + - ``bool -> bool -> bool`` + - Short-circuit or + +The operators ``/\`` and ``&&`` both denote conjunction, and ``\/`` +and ``||`` both denote disjunction. The difference is that ``&&`` and +``||`` are *short-circuit* (the second argument is not evaluated if +the first determines the result), while ``/\`` and ``\/`` are +symmetric. In practice, ``/\`` and ``\/`` are used in logical +formulas, while ``&&`` and ``||`` appear in programs. + +------------------------------------------------------------------------ +Tuples and projections +------------------------------------------------------------------------ + +Tuple expressions are written with parentheses and commas: + +.. code-block:: easycrypt + + (1, true) (* int * bool *) + (1, 2, 3) (* int * int * int *) + +Components are accessed by projection, written with a backtick and a +1-based index: + +.. code-block:: easycrypt + + (1, true).`1 (* = 1 *) + (1, true).`2 (* = true *) + +For pairs, the standard library provides ``fst`` and ``snd``. + +------------------------------------------------------------------------ +Records +------------------------------------------------------------------------ + +Record values are constructed with ``{|`` and ``|}`` delimiters, +listing field assignments: + +.. code-block:: easycrypt + + type point = { x : int; y : int; }. + + op origin : point = {| x = 0; y = 0; |}. + +Fields are accessed with backtick-field syntax: + +.. code-block:: easycrypt + + op get_x (p : point) : int = p.`x. + +A record can be updated functionally using ``with``: + +.. code-block:: easycrypt + + op move_right (p : point) : point = {| p with x = p.`x + 1; |}. + +------------------------------------------------------------------------ +Constructors and pattern matching +------------------------------------------------------------------------ + +Values of algebraic datatypes are built by applying constructors: + +.. code-block:: easycrypt + + Some 42 (* : int option *) + None (* : 'a option *) + Red (* : color *) + +The ``match`` expression inspects a value of an algebraic datatype +and branches based on its constructor: + +.. code-block:: easycrypt + + match ox with + | None => 0 + | Some x => x + 1 + end. + +Patterns can be nested and can bind variables: + +.. code-block:: easycrypt + + match ot with + | Leaf => 0 + | Node x Leaf _ => x + | Node x _ _ => x + 1 + end. + +The ``match`` must be exhaustive: every constructor must be covered. + +------------------------------------------------------------------------ +List syntax +------------------------------------------------------------------------ + +Lists have special syntactic support. The empty list is ``[]`` and +the cons operator is ``::``: + +.. code-block:: easycrypt + + [] (* empty list *) + 1 :: 2 :: 3 :: [] (* [1; 2; 3] *) + [1; 2; 3] (* same as above *) + +List operations are provided by the ``List`` theory (see +:ref:`language-stdlib`). + +------------------------------------------------------------------------ +Let bindings +------------------------------------------------------------------------ + +A ``let`` expression introduces a local definition: + +.. code-block:: easycrypt + + let x = 2 + 3 in x * x. (* = 25 *) + +Patterns are supported on the left-hand side: + +.. code-block:: easycrypt + + let (x, y) = (1, 2) in x + y. (* = 3 *) + +------------------------------------------------------------------------ +Conditionals +------------------------------------------------------------------------ + +The ``if-then-else`` expression selects between two branches based on +a boolean condition: + +.. code-block:: easycrypt + + if 0 < x then x else -x. + +The ``else`` branch is mandatory. Both branches must have the same +type. + +------------------------------------------------------------------------ +Lambda abstractions +------------------------------------------------------------------------ + +Anonymous functions are written with the ``fun`` keyword: + +.. code-block:: easycrypt + + fun x => x + 1 (* int -> int *) + fun (x : int) => x + 1 (* with annotation *) + fun x y => x + y (* int -> int -> int *) + fun (x y : int) => x + y (* with annotation *) + +Lambdas are first-class: they can be passed to operators, stored in +data structures, and returned from other operators. + +.. code-block:: easycrypt + + op succ : int -> int = fun x => x + 1. + +------------------------------------------------------------------------ +Quantifiers +------------------------------------------------------------------------ + +Universal and existential quantifiers bind variables and range over +all values of their type: + +.. code-block:: easycrypt + + forall (x : int), 0 <= x * x. + exists (y : int), y * y = 4. + +The parenthesized type annotation is optional when the type can be +inferred: + +.. code-block:: easycrypt + + forall x, x = x. + +Multiple variables can be bound at once: + +.. code-block:: easycrypt + + forall (x y : int), x + y = y + x. + +Quantifiers associate to the right and extend as far as possible: + +.. code-block:: easycrypt + + forall x, forall y, x + y = y + x. + (* is the same as *) + forall (x y : int), x + y = y + x. + +------------------------------------------------------------------------ +Type annotations +------------------------------------------------------------------------ + +Any expression can be annotated with a type using a colon: + +.. code-block:: easycrypt + + (42 : int) + (fun x => x : int -> int) + +Type annotations are useful for resolving ambiguities when EasyCrypt's +type inference cannot determine the type on its own, for instance with +polymorphic operators. + +------------------------------------------------------------------------ +Map operations +------------------------------------------------------------------------ + +EasyCrypt provides special syntax for functional map (association) +operations. Given a function ``f : 'a -> 'b``: + +.. code-block:: easycrypt + + f.[x] (* lookup: f x *) + f.[x <- v] (* update: fun y => if y = x then v else f y *) + +These are defined in the ``Logic`` prelude and work on any function +type. The ``SmtMap`` and ``FMap`` theories provide more structured +map types with their own operations. diff --git a/doc/language/05-formulas.rst b/doc/language/05-formulas.rst new file mode 100644 index 0000000000..9dc200c95b --- /dev/null +++ b/doc/language/05-formulas.rst @@ -0,0 +1,239 @@ +.. _language-formulas: + +======================================================================== +Formulas +======================================================================== + +Formulas are the language of propositions in EasyCrypt. A formula is +an expression of type ``bool`` -- there is no separate sort for +propositions. This means that all the expression syntax from +:ref:`language-expressions` is available inside formulas: arithmetic, +function application, pattern matching, etc. + +What distinguishes formulas from plain expressions is a set of +additional constructs for referring to program state (memories, +program variables, probabilities) and for expressing judgments in +the program logics. + +.. contents:: + :local: + +------------------------------------------------------------------------ +Logical connectives +------------------------------------------------------------------------ + +The logical connectives were listed in +:ref:`language-expressions` under boolean operators, but they bear +repeating here since they are the backbone of formulas: + +.. code-block:: easycrypt + + P /\ Q (* conjunction *) + P \/ Q (* disjunction *) + P => Q (* implication *) + P <=> Q (* equivalence *) + ! P (* negation *) + + true (* tautology *) + false (* absurdity *) + +These are regular boolean operators. Implication ``=>`` associates +to the right: ``P => Q => R`` means ``P => (Q => R)``. + +Quantifiers +~~~~~~~~~~~ + +.. code-block:: easycrypt + + forall (x : t), P x (* universal *) + exists (x : t), P x (* existential *) + +Multiple binders: + +.. code-block:: easycrypt + + forall (x y : int) (b : bool), ... + +------------------------------------------------------------------------ +Equality +------------------------------------------------------------------------ + +Equality is polymorphic and decidable for every type: + +.. code-block:: easycrypt + + x = y (* equality *) + x <> y (* disequality, abbreviation for !(x = y) *) + +------------------------------------------------------------------------ +Program variable references +------------------------------------------------------------------------ + +Inside formulas, you can refer to the values of program variables +at specific *memories* (snapshots of program state). This is +essential for stating pre- and post-conditions. + +In a **Hoare** judgment, the memory is implicit: + +- Program variables in the precondition refer to the initial state. +- Program variables in the postcondition refer to the final state. +- The special identifier ``res`` refers to the return value in + postconditions. + +In a **relational** judgment (``equiv`` / ``pRHL``), there are two +memories -- the *left* memory and the *right* memory -- distinguished +by tags: + +.. code-block:: easycrypt + + x{1} (* variable x in the left memory *) + x{2} (* variable x in the right memory *) + + glob M{1} (* global state of module M, left side *) + glob M{2} (* global state of module M, right side *) + + res{1} (* return value of the left procedure *) + res{2} (* return value of the right procedure *) + +In non-relational contexts (Hoare logic), program variables carry +no tag: + +.. code-block:: easycrypt + + x (* in hoare pre/postconditions *) + +------------------------------------------------------------------------ +Module state in formulas +------------------------------------------------------------------------ + +The expression ``glob M`` denotes the tuple of all global variables +of module ``M`` (and its sub-modules). It is a first-class value +that can be compared, stored, and quantified over: + +.. code-block:: easycrypt + + glob M{1} = glob M{2} (* the two sides have the same state *) + +The type of ``glob M`` depends on the variables declared in ``M``. + +------------------------------------------------------------------------ +Probability expressions +------------------------------------------------------------------------ + +EasyCrypt can express the probability of an event after running a +procedure. The general syntax is: + +.. code-block:: easycrypt + + Pr[M.f(args) @ &m : event] + +where: + +- ``M.f(args)`` is a procedure call with concrete arguments. +- ``&m`` is a *memory identifier*, representing the initial state. +- ``event`` is a boolean formula over program variables, representing + the event whose probability is being measured. + +Examples: + +.. code-block:: easycrypt + + Pr[Game.main() @ &m : res] + Pr[Game.main() @ &m : res /\ Game.x = 0] + +The result is a ``real`` value between 0 and 1. + +To use probability expressions in lemma statements, you typically +quantify over the initial memory: + +.. code-block:: easycrypt + + lemma example &m : Pr[Game.main() @ &m : res] = 1%r / 2%r. + +------------------------------------------------------------------------ +Hoare judgments +------------------------------------------------------------------------ + +EasyCrypt supports several program logics, each with its own judgment +form. These can appear as top-level lemma statements or as +sub-formulas. + +Hoare logic (HL) +~~~~~~~~~~~~~~~~ + +.. code-block:: easycrypt + + hoare[M.f : pre ==> post] + +States that if the precondition ``pre`` holds before calling ``M.f``, +then the postcondition ``post`` holds after ``M.f`` terminates. In +``post``, the identifier ``res`` refers to the return value. + +Probabilistic Hoare logic (pHL) +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. code-block:: easycrypt + + phoare[M.f : pre ==> post] >= p + phoare[M.f : pre ==> post] <= p + phoare[M.f : pre ==> post] = p + +Like Hoare logic, but the postcondition is satisfied with a given +probability bound ``p``. + +A special case is losslessness (the procedure terminates with +probability 1): + +.. code-block:: easycrypt + + islossless M.f + +This is equivalent to ``phoare[M.f : true ==> true] = 1%r``. + +Probabilistic relational Hoare logic (pRHL) +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. code-block:: easycrypt + + equiv[M.f ~ N.g : pre ==> post] + +States that for any initial states satisfying ``pre``, the final +states of ``M.f`` and ``N.g`` satisfy ``post`` with equal +probability. The precondition and postcondition can refer to +variables on both sides using the ``{1}`` and ``{2}`` tags. + +Eager Hoare logic (eHL) +~~~~~~~~~~~~~~~~~~~~~~~~ + +.. code-block:: easycrypt + + ehoare[M.f : pre ==> post] + +Used for reasoning about expected values and costs. The postcondition +is an *extended real* expression (possibly involving ``+oo``), and +the judgment bounds the expected value of the postcondition. + +------------------------------------------------------------------------ +Putting it together +------------------------------------------------------------------------ + +Here is an example of a complete lemma statement involving a +relational judgment: + +.. code-block:: easycrypt + + lemma example : + equiv[Game0.main ~ Game1.main : + ={glob Game0, glob Game1} ==> + ={res}]. + +This states that ``Game0.main`` and ``Game1.main`` produce the same +return value (``={res}`` is syntactic sugar for ``res{1} = res{2}``) +whenever they start from the same global state. + +The ``={}`` notation is a convenient shorthand for pointwise equality: + +.. code-block:: easycrypt + + ={x, y} (* x{1} = x{2} /\ y{1} = y{2} *) + ={glob M} (* glob M{1} = glob M{2} *) diff --git a/doc/language/06-programs.rst b/doc/language/06-programs.rst new file mode 100644 index 0000000000..79370ae898 --- /dev/null +++ b/doc/language/06-programs.rst @@ -0,0 +1,281 @@ +.. _language-programs: + +======================================================================== +Programs +======================================================================== + +EasyCrypt has an imperative programming language for describing +algorithms. Programs live inside *modules* (see +:ref:`language-modules`): a module declares mutable global variables +and *procedures* that operate on them. + +This chapter describes the statement language used inside procedures. +The focus is on the syntax of individual statements; modules +themselves are covered in the next chapter. + +.. contents:: + :local: + +------------------------------------------------------------------------ +Procedures +------------------------------------------------------------------------ + +A procedure is declared inside a module with the ``proc`` keyword. +It has a name, parameters, a return type, and a body: + +.. code-block:: easycrypt + + module M = { + proc add (x y : int) : int = { + var r : int; + r <- x + y; + return r; + } + }. + +The body is a block of statements enclosed in braces. + +The return type can be ``unit`` for procedures that do not return a +meaningful value. In that case, the ``return`` statement can be +omitted. + +------------------------------------------------------------------------ +Variable declarations +------------------------------------------------------------------------ + +Local variables are declared at the beginning of a procedure body +with the ``var`` keyword: + +.. code-block:: easycrypt + + var x : int; + var y, z : bool; + var r : int <- 0; (* with initializer *) + +Multiple variables of the same type can be declared together. +Variables can optionally be given an initial value with ``<-``. +Uninitialized variables start with an arbitrary value of their type. + +Global (module-level) variables are declared inside a module but +outside any procedure: + +.. code-block:: easycrypt + + module M = { + var count : int (* global variable *) + + proc incr () : unit = { + count <- count + 1; + } + }. + +Global variables persist across procedure calls and are part of the +module's state. + +------------------------------------------------------------------------ +Assignments +------------------------------------------------------------------------ + +A deterministic assignment stores a value in a variable: + +.. code-block:: easycrypt + + x <- 42; + x <- x + 1; + (a, b) <- (b, a); (* tuple assignment / swap *) + +The left-hand side is a variable name (or a tuple of variable names +for simultaneous assignment). + +------------------------------------------------------------------------ +Random sampling +------------------------------------------------------------------------ + +The sampling statement draws a value from a distribution and stores +it in a variable: + +.. code-block:: easycrypt + + x <$ d; + +Here ``d`` is an expression of type ``'a distr``. After the +statement, ``x`` holds a random value drawn according to ``d``. + +Common distributions (from the standard library): + +.. code-block:: easycrypt + + x <$ duniform l; (* uniform over list l *) + b <$ dbool; (* fair coin flip *) + n <$ [0..k-1]; (* uniform integer in range *) + +The ``<$`` operator is what makes EasyCrypt programs *probabilistic*. +All randomness must be introduced through sampling. + +------------------------------------------------------------------------ +Procedure calls +------------------------------------------------------------------------ + +A procedure call invokes a procedure and (optionally) stores the +result: + +.. code-block:: easycrypt + + r <@ M.f(x, y); (* call M.f, store result in r *) + M.g(); (* call M.g, discard result *) + +The ``<@`` operator indicates a procedure call (as opposed to ``<-`` +for deterministic assignment or ``<$`` for sampling). + +Tuple unpacking works on the left-hand side: + +.. code-block:: easycrypt + + (a, b) <@ M.pair_proc(x); + +------------------------------------------------------------------------ +Conditionals +------------------------------------------------------------------------ + +.. code-block:: easycrypt + + if (condition) { + (* then-branch statements *) + } else { + (* else-branch statements *) + } + +The ``else`` branch is optional. Braces are mandatory even for +single-statement branches. + +There is also an ``elif`` form: + +.. code-block:: easycrypt + + if (x < 0) { + r <- -1; + } elif (x = 0) { + r <- 0; + } else { + r <- 1; + } + +------------------------------------------------------------------------ +While loops +------------------------------------------------------------------------ + +.. code-block:: easycrypt + + while (condition) { + (* loop body *) + } + +The loop executes the body repeatedly as long as the condition holds. + +.. note:: + + EasyCrypt does not have a ``for`` loop construct. Bounded + iteration is typically done with a ``while`` loop and a counter, + or at the logical level using recursion on lists or ranges. + +------------------------------------------------------------------------ +Pattern matching +------------------------------------------------------------------------ + +A ``match`` statement branches on the constructor of an algebraic +datatype: + +.. code-block:: easycrypt + + match ox with + | None => { + r <- 0; + } + | Some x => { + r <- x; + } + end; + +Each branch is a block of statements. + +------------------------------------------------------------------------ +Exceptions +------------------------------------------------------------------------ + +EasyCrypt supports exceptions in the imperative fragment. + +Declaring exceptions +~~~~~~~~~~~~~~~~~~~~ + +New exception constructors are declared at the top level: + +.. code-block:: easycrypt + + exception Error. + exception Timeout of int. + +Exception constructors are values of type ``exn`` and can carry +arguments (like datatype constructors). + +Raising exceptions +~~~~~~~~~~~~~~~~~~ + +The ``raise`` statement aborts the current procedure with an +exception: + +.. code-block:: easycrypt + + raise Error; + raise (Timeout 42); + +Note: exception handling (``try``/``catch``) is limited in EasyCrypt. +Exceptions are mainly used as a modeling tool for certain +code-transformation arguments in proofs. + +------------------------------------------------------------------------ +Program variables vs. logical variables +------------------------------------------------------------------------ + +It is important to distinguish the two kinds of variables in +EasyCrypt: + +**Program variables** are mutable. They exist inside module +procedures and change as the program executes. In formulas, they +refer to the value at a specific point in execution (initial state, +final state, left/right memory). + +**Logical variables** are immutable. They are bound by quantifiers +(``forall``, ``exists``), ``let`` expressions, or as parameters of +operators and lemmas. They do not change. + +In formulas, program variables can be tagged with a memory +(``x{1}``, ``x{2}``) to specify which execution point they refer to. +Logical variables never carry memory tags. + +Inside a procedure body, all variables are program variables. In a +lemma statement or operator definition, all variables are logical. +The two worlds meet in pre- and postconditions of Hoare judgments, +where program variables refer to concrete execution state and logical +variables act as parameters or ghost state. + +------------------------------------------------------------------------ +Return values +------------------------------------------------------------------------ + +A procedure returns a value using the ``return`` statement: + +.. code-block:: easycrypt + + proc f (x : int) : int = { + return x + 1; + } + +In postconditions, the keyword ``res`` refers to the return value: + +.. code-block:: easycrypt + + hoare[M.f : x = 5 ==> res = 6] + +If a procedure does not have an explicit ``return``, the return value +is the last assigned value of the ``res`` local variable (implicitly +declared), or ``witness`` if nothing was assigned. diff --git a/doc/language/07-modules.rst b/doc/language/07-modules.rst new file mode 100644 index 0000000000..98b1211e61 --- /dev/null +++ b/doc/language/07-modules.rst @@ -0,0 +1,250 @@ +.. _language-modules: + +======================================================================== +Modules +======================================================================== + +Modules are the mechanism for packaging mutable state and procedures +together. They play a central role in EasyCrypt: cryptographic +schemes, adversaries, oracles, and security games are all modeled as +modules. + +.. contents:: + :local: + +------------------------------------------------------------------------ +Module types +------------------------------------------------------------------------ + +A *module type* (also called a *signature* or *interface*) declares +the procedures a module must provide, without specifying their +implementation: + +.. code-block:: easycrypt + + module type Adv = { + proc guess(c : cipher) : key + }. + +This declares an interface ``Adv`` with a single procedure ``guess`` +that takes a ``cipher`` and returns a ``key``. + +Module types can declare several procedures: + +.. code-block:: easycrypt + + module type Oracle = { + proc init() : unit + proc query(x : int) : int + }. + +Procedure declarations in a module type do not have bodies -- only +names, parameters, and return types. + +Including other module types +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +A module type can include another module type to inherit its +procedure declarations: + +.. code-block:: easycrypt + + module type ExtOracle = { + include Oracle + proc reset() : unit + }. + +This gives ``ExtOracle`` all the procedures of ``Oracle`` plus an +additional ``reset`` procedure. + +A restriction clause can limit which procedures are included: + +.. code-block:: easycrypt + + module type Limited = { + include Oracle [query] (* only include query, not init *) + }. + +------------------------------------------------------------------------ +Concrete modules +------------------------------------------------------------------------ + +A concrete module implements a module type by providing variable +declarations and procedure bodies: + +.. code-block:: easycrypt + + module M : Oracle = { + var table : (int, int) fmap + + proc init() : unit = { + table <- empty; + } + + proc query(x : int) : int = { + var r : int; + r <$ [0..100]; + if (x \notin table) { + table.[x] <- r; + } + return oget table.[x]; + } + }. + +The ``: Oracle`` annotation is optional. If present, EasyCrypt checks +that the module provides all procedures required by the module type. + +Global variables (``var``) are part of the module's state. They +persist across procedure calls and can be read or written by any +procedure in the module. + +------------------------------------------------------------------------ +Functors +------------------------------------------------------------------------ + +A *functor* is a module that is parameterized by other modules. This +is the standard way to model algorithms that interact with an +adversary or oracle. + +.. code-block:: easycrypt + + module Game (A : Adv) (O : Oracle) = { + proc main() : bool = { + var k, k' : key; + var c : cipher; + + O.init(); + k <$ dkey; + c <- encrypt k m; + k' <@ A.guess(c); + return (k = k'); + } + }. + +Here ``Game`` is parameterized by an adversary ``A`` of type ``Adv`` +and an oracle ``O`` of type ``Oracle``. The procedures of ``A`` and +``O`` can be called inside the body of ``Game``. + +Functors are *applied* (instantiated) by supplying concrete modules: + +.. code-block:: easycrypt + + module ConcreteGame = Game(ConcreteAdv, ConcreteOracle). + +The result ``ConcreteGame`` is a concrete module with no remaining +parameters. + +------------------------------------------------------------------------ +Module restrictions +------------------------------------------------------------------------ + +When a module type is used as a functor parameter, you often want to +restrict which other modules the parameter can access. This prevents +an adversary from, say, calling an oracle it should not have access to. + +Restrictions are specified with a set annotation on the module type: + +.. code-block:: easycrypt + + module type Adv = { + proc guess(c : cipher) : key + }. + + module Game (A : Adv {-Game}) = { ... }. + +The ``{-Game}`` restriction says that ``A`` must not access the +global state of ``Game``. The syntax ``{+M}`` means "may access M", +and ``{-M}`` means "must not access M". + +More complex restrictions are possible: + +.. code-block:: easycrypt + + module Game (A : Adv {-Game, +O}) (O : Oracle {-A}) = { ... }. + +Here ``A`` may access ``O`` but not ``Game``, and ``O`` may not +access ``A``. + +Restrictions are critical for the soundness of game-based proofs: +they ensure that adversaries interact only through the intended +interfaces. + +------------------------------------------------------------------------ +Abstract modules +------------------------------------------------------------------------ + +Inside a *section*, you can declare an abstract module -- a module +whose implementation is unknown but whose type is given: + +.. code-block:: easycrypt + + section. + declare module A <: Adv. + (* ... lemmas about A ... *) + end section. + +The ``declare module`` statement introduces ``A`` as a module of type +``Adv`` without fixing its implementation. This is analogous to an +abstract type: you can use ``A`` in procedure calls and formulas, but +you know nothing about it beyond what the module type guarantees. + +When the section is closed, all lemmas that use ``A`` are +automatically universally quantified over all modules of type ``Adv``. + +Abstract modules can also carry restrictions: + +.. code-block:: easycrypt + + declare module A <: Adv {-Game, -O}. + +------------------------------------------------------------------------ +Module state +------------------------------------------------------------------------ + +The state of a module is the collection of its global variables. In +formulas, the expression ``glob M`` refers to the current value of +all global variables of module ``M`` (packaged as a tuple). + +.. code-block:: easycrypt + + glob Game (* the state of module Game *) + glob A (* the state of abstract module A *) + +This is useful for writing pre- and postconditions: + +.. code-block:: easycrypt + + equiv[Game(A).main ~ Game(A).main : + ={glob A, glob Game} ==> ={res}]. + +The type of ``glob M`` depends on the variables declared in ``M``. +For abstract modules, the type is also abstract. + +------------------------------------------------------------------------ +Module expressions +------------------------------------------------------------------------ + +Beyond simple module names, EasyCrypt supports several forms of +module expressions: + +Functor application +~~~~~~~~~~~~~~~~~~~ + +.. code-block:: easycrypt + + Game(A, O) + +Applies a functor to its arguments. + +Module restriction +~~~~~~~~~~~~~~~~~~ + +You can restrict a module in expressions to hide some of its +procedures: + +.. code-block:: easycrypt + + module M' = M [query]. + +This creates a module that only exposes the ``query`` procedure of +``M``. diff --git a/doc/language/08-theories.rst b/doc/language/08-theories.rst new file mode 100644 index 0000000000..55151ca491 --- /dev/null +++ b/doc/language/08-theories.rst @@ -0,0 +1,266 @@ +.. _language-theories: + +======================================================================== +Theories and sections +======================================================================== + +EasyCrypt organizes definitions into *theories* and *sections*. +Theories provide namespacing and modularity -- grouping related +definitions under a name that can be required and imported. Sections +provide a scoping mechanism for local assumptions and abstract +declarations. + +.. contents:: + :local: + +------------------------------------------------------------------------ +Theories +------------------------------------------------------------------------ + +A theory groups a sequence of declarations under a common name: + +.. code-block:: easycrypt + + theory Arith. + op double (x : int) = x + x. + + lemma doubleE (x : int) : double x = x + x. + proof. by []. qed. + end Arith. + +After the theory is closed, its contents are accessed through +qualified names: + +.. code-block:: easycrypt + + op y = Arith.double 3. + +You can bring names into scope with ``import``: + +.. code-block:: easycrypt + + import Arith. + op y = double 3. (* no qualification needed *) + +Theories can be nested: + +.. code-block:: easycrypt + + theory Outer. + theory Inner. + op f (x : int) = x. + end Inner. + end Outer. + + op y = Outer.Inner.f 1. + +Local theories +~~~~~~~~~~~~~~ + +A ``local`` theory is not visible outside its enclosing theory: + +.. code-block:: easycrypt + + theory T. + local theory Helper. + op aux (x : int) = x + 1. + end Helper. + + op f (x : int) = Helper.aux (Helper.aux x). + end T. + + (* Helper is not accessible here *) + +------------------------------------------------------------------------ +Abstract theories +------------------------------------------------------------------------ + +An *abstract* theory contains ``axiom`` declarations -- unproven +assumptions. It serves as a template that can be *cloned* (see +:ref:`language-cloning`) with concrete definitions replacing the +abstract ones. + +.. code-block:: easycrypt + + abstract theory Group. + type group. + op e : group. (* identity *) + op ( * ) : group -> group -> group. + op inv : group -> group. + + axiom mulA (x y z : group) : + x * (y * z) = (x * y) * z. + axiom mul1 (x : group) : e * x = x. + axiom mulV (x : group) : inv x * x = e. + + lemma mul1r (x : group) : x * e = x. + proof. (* ... provable from the axioms ... *) admitted. + end Group. + +Abstract theories are the primary mechanism for generic, +reusable mathematics in EasyCrypt. The standard library uses them +extensively for algebraic structures, cryptographic primitives, and +game transformations. + +------------------------------------------------------------------------ +Sections +------------------------------------------------------------------------ + +A *section* opens a local scope in which you can introduce abstract +declarations (types, operators, modules) and local axioms. When the +section is closed, these abstractions are *discharged*: every lemma +proved in the section is generalized over the abstract declarations, +and the local axioms become hypotheses. + +.. code-block:: easycrypt + + section. + declare module A <: Adv {-Game}. + + declare axiom A_ll : islossless A.guess. + + lemma game_result &m : + Pr[Game(A).main() @ &m : res] <= 1%r. + proof. (* ... *) admitted. + end section. + +After the section closes, ``game_result`` becomes: + +.. code-block:: easycrypt + + lemma game_result : + forall (A <: Adv {-Game}), + islossless A.guess => + forall &m, Pr[Game(A).main() @ &m : res] <= 1%r. + +The ``declare`` keyword is used for all section-local abstractions: + +``declare module`` + Introduces an abstract module (with an optional restriction). + +``declare axiom`` + Introduces a local hypothesis that becomes a premise after the + section closes. + +``declare op`` + Introduces an abstract operator local to the section. + +``declare type`` + Introduces an abstract type local to the section. + +Named sections +~~~~~~~~~~~~~~ + +Sections can be given a name: + +.. code-block:: easycrypt + + section Security. + (* ... *) + end section Security. + +This is useful for documentation; it has no semantic effect beyond +matching the open/close delimiters. + +------------------------------------------------------------------------ +Namespaces and qualified names +------------------------------------------------------------------------ + +Every declaration lives in a namespace determined by the enclosing +theories. A fully qualified name has the form: + +.. code-block:: text + + Theory1.Theory2. ... .name + +When you ``import`` a theory, its names become available without +qualification. If two imported theories define the same name, you +must use qualification to disambiguate. + +EasyCrypt resolves names by searching the current scope outward: +local definitions shadow imported ones, and more recently imported +theories take priority over earlier ones. + +------------------------------------------------------------------------ +Require, import, and export +------------------------------------------------------------------------ + +``require`` +~~~~~~~~~~~ + +The ``require`` command loads an external ``.ec`` file and makes it +available as a theory: + +.. code-block:: easycrypt + + require AllCore. + +After this, the contents of ``AllCore`` are accessible via qualified +names (e.g., ``AllCore.List.size``). + +``require import`` +~~~~~~~~~~~~~~~~~~ + +Combines requiring with importing -- names are brought directly into +scope: + +.. code-block:: easycrypt + + require import AllCore. + +This is the most common form. Multiple theories can be required at +once: + +.. code-block:: easycrypt + + require import AllCore List FSet Distr. + +``require export`` +~~~~~~~~~~~~~~~~~~ + +Combines requiring with exporting -- names are not only in scope +locally, but also re-exported to anyone who later imports the +current file: + +.. code-block:: easycrypt + + require export AllCore. + +``import`` and ``export`` (standalone) +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +You can import or export a previously required theory: + +.. code-block:: easycrypt + + require AllCore. + import AllCore. + +Or import a sub-theory: + +.. code-block:: easycrypt + + require AllCore. + import AllCore.List. + +Aliasing on require +~~~~~~~~~~~~~~~~~~~ + +You can rename a theory on require: + +.. code-block:: easycrypt + + require [AllCore as AC]. + +After this, the theory is known as ``AC`` instead of ``AllCore``. + +``from`` clause +~~~~~~~~~~~~~~~ + +The ``from`` clause specifies a search path prefix: + +.. code-block:: easycrypt + + require from Jasmin MyTheory. + +This is used when theories are organized in subdirectories. diff --git a/doc/language/09-cloning.rst b/doc/language/09-cloning.rst new file mode 100644 index 0000000000..f5667b279b --- /dev/null +++ b/doc/language/09-cloning.rst @@ -0,0 +1,274 @@ +.. _language-cloning: + +======================================================================== +Cloning +======================================================================== + +*Cloning* is the mechanism for instantiating abstract theories with +concrete definitions. It creates a copy of a theory in which +abstract types, operators, predicates, and axioms are replaced by +concrete ones. Lemmas proved in the original theory carry over to +the clone, provided the axioms they depend on are discharged. + +Cloning is one of the most powerful features of EasyCrypt and is used +extensively in the standard library and in real-world proofs. + +.. contents:: + :local: + +------------------------------------------------------------------------ +Basic cloning +------------------------------------------------------------------------ + +The simplest form of cloning copies a theory under a new name: + +.. code-block:: easycrypt + + clone Foo as Bar. + +This creates a copy of theory ``Foo`` named ``Bar``. Everything in +``Bar`` is identical to ``Foo`` -- the names are just prefixed +differently. + +More commonly, you clone a theory while providing concrete +definitions for its abstract components. Consider an abstract theory: + +.. code-block:: easycrypt + + abstract theory Monoid. + type t. + op e : t. + op (+) : t -> t -> t. + + axiom addA (x y z : t) : x + (y + z) = (x + y) + z. + axiom add0 (x : t) : e + x = x. + end Monoid. + +You clone it by specifying the type and operations: + +.. code-block:: easycrypt + + clone Monoid as IntAdd with + type t = int, + op e = 0, + op (+) = Int.(+) + proof. + realize addA. by smt(). qed. + realize add0. by smt(). qed. + qed. + +The ``with`` clause provides concrete replacements for abstract +items. The ``proof`` block discharges the axioms of the original +theory by proving they hold for the concrete definitions. + +------------------------------------------------------------------------ +Overriding types, operators, and predicates +------------------------------------------------------------------------ + +The ``with`` clause supports several forms of override. + +Type overrides +~~~~~~~~~~~~~~ + +.. code-block:: easycrypt + + clone T as T' with + type key = int, + type 'a container = 'a list. + +Operator overrides +~~~~~~~~~~~~~~~~~~ + +.. code-block:: easycrypt + + clone T as T' with + op f = fun (x : int) => x + 1, + op g (x : int) = x * 2. + +Predicate overrides +~~~~~~~~~~~~~~~~~~~ + +.. code-block:: easycrypt + + clone T as T' with + pred P (x : int) = 0 < x. + +Override modes +~~~~~~~~~~~~~~ + +There are several override operators: + +- ``=`` -- defines the abstract item as an alias for the given + expression. The original name becomes transparent. + +- ``<-`` -- defines the item *inline* and removes the original + abstract name. + +- ``<=`` -- defines the item inline but keeps the original name. + +In most cases, ``=`` is what you want. + +------------------------------------------------------------------------ +Renaming and removing +------------------------------------------------------------------------ + +Renaming +~~~~~~~~ + +The ``rename`` clause renames items in the clone: + +.. code-block:: easycrypt + + clone T as T' with ... + rename op "old_name" as "new_name". + +You can rename types, operators, predicates, lemmas, exceptions, +modules, module types, and theories. The string arguments are +matched as regular expressions, which allows bulk renaming: + +.. code-block:: easycrypt + + rename lemma "foo_" as "bar_". (* renames foo_X to bar_X *) + +Removing +~~~~~~~~ + +The ``remove`` clause removes abbreviations from the clone: + +.. code-block:: easycrypt + + clone T as T' with ... + remove abbrev ( * ). + +This is useful when the clone provides its own notation and the +original abbreviations would cause conflicts. + +------------------------------------------------------------------------ +Proof obligations +------------------------------------------------------------------------ + +When an abstract theory has axioms, cloning it generates *proof +obligations* -- you must prove that the axioms hold for your concrete +definitions. + +The proof block after a ``clone`` uses ``realize`` to discharge each +axiom: + +.. code-block:: easycrypt + + clone Monoid as IntMul with + type t = int, + op e = 1, + op (+) = Int.( * ) + proof. + realize addA. by smt(). qed. + realize add0. by smt(). qed. + qed. + +If you want to leave some axioms unproven (keeping them as axioms in +the clone), you can omit their ``realize`` or use ``admit``: + +.. code-block:: easycrypt + + proof. realize addA. by smt(). qed. qed. + (* add0 is not realized, so it remains an axiom in the clone *) + +Proof tags +~~~~~~~~~~ + +You can selectively include or exclude axioms from the proof +obligation using tags. Axioms can be tagged in the original theory: + +.. code-block:: easycrypt + + axiom [mytag] foo : ... + +And the clone can filter by tag: + +.. code-block:: easycrypt + + clone T as T' with ... proof *. (* prove all *) + clone T as T' with ... proof -. (* prove none *) + +------------------------------------------------------------------------ +Common cloning patterns +------------------------------------------------------------------------ + +Instantiating algebraic structures +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The standard library defines abstract theories for rings, fields, +ordered types, etc. These are instantiated by cloning: + +.. code-block:: easycrypt + + require import Ring. + + clone ComRing as IntRing with + type t = int, + op zeror = 0, + op oner = 1, + op (+) = Int.(+), + op ( * ) = Int.( * ), + op [-] = Int.([-]) + proof. (* ... *) qed. + +Instantiating finite types +~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The ``FinType`` theory defines the notion of a finite type with +enumeration. To declare that your type is finite: + +.. code-block:: easycrypt + + require import FinType. + + clone FinType as BoolFin with + type t = bool, + op enum = [true; false] + proof. (* ... *) qed. + +Instantiating cryptographic primitives +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The ``PROM`` theory provides a programmable random oracle model. +Cloning it sets up the oracle for your specific key/hash types: + +.. code-block:: easycrypt + + require import PROM. + + clone FullRO as RO with + type in_t = msg, + type out_t = hash, + op dout _ = dhash + proof. (* ... *) qed. + +------------------------------------------------------------------------ +Clone without ``as`` +------------------------------------------------------------------------ + +If you omit the ``as`` clause, the contents of the clone are +imported directly into the current scope (like an anonymous clone): + +.. code-block:: easycrypt + + clone Monoid with + type t = int, + op e = 0, + op (+) = Int.(+) + proof. (* ... *) qed. + +This is convenient but can cause name clashes. Using ``as`` to give +the clone an explicit name is generally safer. + +------------------------------------------------------------------------ +Local clones +------------------------------------------------------------------------ + +A clone can be declared ``local``, making it visible only within the +enclosing theory: + +.. code-block:: easycrypt + + local clone Monoid as M with ... proof. ... qed. diff --git a/doc/language/10-hints-printing.rst b/doc/language/10-hints-printing.rst new file mode 100644 index 0000000000..57c564718c --- /dev/null +++ b/doc/language/10-hints-printing.rst @@ -0,0 +1,195 @@ +.. _language-hints: + +======================================================================== +Hints, printing, and configuration +======================================================================== + +Beyond definitions and proofs, EasyCrypt provides commands for +configuring automated reasoning, inspecting the environment, and +controlling the prover. + +.. contents:: + :local: + +------------------------------------------------------------------------ +Hint databases +------------------------------------------------------------------------ + +EasyCrypt maintains several databases of lemmas that automated tactics +can draw from. The ``hint`` command registers lemmas in these +databases. + +Simplification hints +~~~~~~~~~~~~~~~~~~~~ + +The ``simplify`` tactic uses a database of rewrite rules to +normalize terms. You add rules with: + +.. code-block:: easycrypt + + hint simplify lemma1, lemma2. + +This registers ``lemma1`` and ``lemma2`` as simplification rules: +whenever ``simplify`` runs, it tries to apply these lemmas as +left-to-right rewrites. + +The standard library uses this extensively: + +.. code-block:: easycrypt + + hint simplify oget_some, oget_none. + +Rewriting hints +~~~~~~~~~~~~~~~ + +The rewriting database is used by tactics that search for applicable +rewrite lemmas: + +.. code-block:: easycrypt + + hint rewrite mydb : lemma1 lemma2 lemma3. + +This creates (or extends) a named rewrite database ``mydb`` with the +given lemmas. You can then use it: + +.. code-block:: easycrypt + + rewrite mydb. (* applies any lemma from mydb that matches *) + +Solve hints +~~~~~~~~~~~ + +The ``solve`` hint database is used by the ``solve`` tactic to +discharge goals automatically: + +.. code-block:: easycrypt + + hint solve 0 : lemma1 lemma2. + +The number (here ``0``) is a priority. Priority ``0`` means the +lemma must match exactly (no unification); higher priorities allow +more flexibility. + +------------------------------------------------------------------------ +Print, search, and locate +------------------------------------------------------------------------ + +These commands help you explore what is available in the current +environment. + +``print`` +~~~~~~~~~ + +Displays the definition and type of an item: + +.. code-block:: easycrypt + + print op double. (* shows the definition of double *) + print type color. (* shows the definition of color *) + print axiom mulA. (* shows the statement of mulA *) + print module type Adv. (* shows the Adv interface *) + print module M. (* shows the structure of module M *) + print theory Ring. (* shows the contents of theory Ring *) + +``search`` +~~~~~~~~~~ + +Searches for lemmas whose statement matches a pattern: + +.. code-block:: easycrypt + + search ( + ). (* lemmas mentioning addition *) + search (_ + _ = _ + _). (* lemmas with a specific shape *) + search [-some_tag]. (* excluding tagged lemmas *) + +``search`` is invaluable for discovering relevant lemmas in the +standard library. + +``locate`` +~~~~~~~~~~ + +Finds the fully qualified name of an identifier: + +.. code-block:: easycrypt + + locate size. (* finds e.g. List.size, FSet.card *) + +------------------------------------------------------------------------ +Prover configuration +------------------------------------------------------------------------ + +EasyCrypt relies on external SMT solvers (such as Z3, CVC4, Alt-Ergo) +to discharge proof obligations. The ``smt`` tactic sends the current +goal to these solvers. + +Configuring provers +~~~~~~~~~~~~~~~~~~~ + +The ``prover`` command controls which solvers are available and how +they are invoked: + +.. code-block:: easycrypt + + prover timeout=5. (* set timeout to 5 seconds *) + prover maxprovers=4. (* use up to 4 solvers in parallel *) + prover [z3 cvc4]. (* use only z3 and cvc4 *) + +Solver hints +~~~~~~~~~~~~ + +You can guide ``smt`` by providing lemmas as hints: + +.. code-block:: easycrypt + + smt(lemma1 lemma2). (* provide these lemmas to the solver *) + +This is often necessary for non-trivial goals: the solver may not +find the right lemmas on its own, but succeeds when given a hint. + +------------------------------------------------------------------------ +Pragmas +------------------------------------------------------------------------ + +Pragmas control various aspects of EasyCrypt's behavior. They are +set with the ``pragma`` command: + +.. code-block:: easycrypt + + pragma Proofs:weak. (* accept unfinished proofs *) + pragma Proofs:check. (* require all proofs (default) *) + +Common pragmas: + +``Proofs:weak`` + Allows ``admit`` and ``admitted`` without warning. Useful during + proof development. + +``Proofs:check`` + The default mode: all proofs must be completed. + +``noia`` + Disables automatic iota-reduction. + +------------------------------------------------------------------------ +Timeout and resource control +------------------------------------------------------------------------ + +You can wrap commands in a ``timeout`` block to limit execution time: + +.. code-block:: easycrypt + + timeout 10 smt. (* give smt 10 seconds *) + +------------------------------------------------------------------------ +Dump and debug +------------------------------------------------------------------------ + +For debugging, EasyCrypt provides: + +.. code-block:: easycrypt + + print. (* print current goal *) + debug. (* enter debug mode *) + +The ``dump`` command can output intermediate proof state for +inspection. diff --git a/doc/language/11-stdlib.rst b/doc/language/11-stdlib.rst new file mode 100644 index 0000000000..c533414f89 --- /dev/null +++ b/doc/language/11-stdlib.rst @@ -0,0 +1,361 @@ +.. _language-stdlib: + +======================================================================== +Standard library tour +======================================================================== + +EasyCrypt comes with a substantial standard library covering +mathematics, data structures, probability, algebra, and cryptographic +definitions. This chapter gives a guided tour of the most commonly +used theories. + +Most EasyCrypt files start with: + +.. code-block:: easycrypt + + require import AllCore. + +which brings the core theories into scope. For specific needs, you +require additional theories. + +.. contents:: + :local: + +------------------------------------------------------------------------ +AllCore +------------------------------------------------------------------------ + +``AllCore`` is the standard entry point. It re-exports: + +- ``Core`` -- basic operations on pairs, options, functions. +- ``Int`` -- integer arithmetic (from ``CoreInt`` and others). +- ``Real`` -- real number arithmetic (from ``CoreReal`` and others). +- ``Xint`` -- extended integers (integers plus infinity). +- ``Ring.IntID`` -- the integer ring instance. + +After ``require import AllCore``, you have access to: + +- Pair operations: ``fst``, ``snd``. +- Option operations: ``oget``, ``omap``, ``obind``, ``odflt``, + ``is_none``, ``is_some``. +- Function operations: ``idfun`` (identity), ``\o`` (composition), + ``(==)`` (extensional equality). +- Map update syntax: ``f.[x <- v]``. +- Integer arithmetic: ``+``, ``-``, ``*``, comparisons. +- Real arithmetic: ``+``, ``-``, ``*``, ``/``, ``inv``. +- Extended integers: ``N`` (finite), ``+oo`` (infinity), operations. +- The ``witness`` constant (default value for any type). + +------------------------------------------------------------------------ +Lists +------------------------------------------------------------------------ + +.. code-block:: easycrypt + + require import List. + +The ``List`` theory provides the type ``'a list`` with: + +Construction and destruction +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +- ``[]`` -- the empty list. +- ``::`` -- cons: ``x :: xs``. +- ``[x1; x2; ...]`` -- list literal syntax. +- ``head`` -- first element (with a default). +- ``behead`` -- tail of the list. + +Measurement +~~~~~~~~~~~ + +- ``size xs`` -- length of a list. + +Concatenation +~~~~~~~~~~~~~ + +- ``++`` -- append: ``xs ++ ys``. +- ``flatten`` -- concatenate a list of lists. + +Access +~~~~~~ + +- ``nth d xs i`` -- element at index ``i``, default ``d``. +- ``last d xs`` -- last element. + +Transformation +~~~~~~~~~~~~~~ + +- ``map f xs`` -- apply ``f`` to each element. +- ``filter p xs`` -- keep elements satisfying ``p``. +- ``zip xs ys`` -- pair up elements. +- ``unzip xs`` -- split a list of pairs. +- ``rev xs`` -- reverse. + +Searching +~~~~~~~~~ + +- ``mem xs x`` (also ``x \in xs``) -- membership. +- ``has p xs`` -- does any element satisfy ``p``? +- ``all p xs`` -- do all elements satisfy ``p``? +- ``find p xs`` -- first element satisfying ``p``. +- ``count p xs`` -- number of elements satisfying ``p``. +- ``index x xs`` -- index of first occurrence. + +Other +~~~~~ + +- ``undup xs`` -- remove duplicates. +- ``perm_eq xs ys`` -- ``xs`` and ``ys`` are permutations. +- ``iota_ i n`` -- the list ``[i; i+1; ...; i+n-1]``. +- ``range i j`` -- shorthand for ``iota_ i (j - i)``. +- ``nseq n x`` -- list of ``n`` copies of ``x``. +- ``mkseq f n`` -- ``[f 0; f 1; ...; f (n-1)]``. + +------------------------------------------------------------------------ +Finite sets and maps +------------------------------------------------------------------------ + +.. code-block:: easycrypt + + require import FSet. + require import FMap. + require import SmtMap. + +``FSet`` -- finite sets +~~~~~~~~~~~~~~~~~~~~~~~ + +The type ``'a fset`` represents a finite set. Key operations: + +- ``fset0`` -- empty set. +- ``fset1 x`` -- singleton. +- ``x \in s`` -- membership. +- ``s1 `|` s2`` -- union. +- ``s1 `&` s2`` -- intersection. +- ``s1 `\` s2`` -- difference. +- ``card s`` -- cardinality. +- ``oflist xs`` -- set from a list. +- ``elems s`` -- list of elements. + +``FMap`` -- finite maps +~~~~~~~~~~~~~~~~~~~~~~~ + +The type ``('a, 'b) fmap`` represents a finite map. Key operations: + +- ``empty`` -- empty map. +- ``m.[x]`` -- lookup (returns ``'b option``). +- ``m.[x <- v]`` -- update. +- ``rem m x`` -- remove a key. +- ``dom m`` -- domain (as a finite set). +- ``rng m`` -- range (as a finite set). + +``SmtMap`` -- SMT-friendly maps +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +``SmtMap`` provides a simpler map type that works well with SMT +solvers. It is often preferred over ``FMap`` for straightforward +map reasoning because SMT can handle it more easily. + +------------------------------------------------------------------------ +Distributions +------------------------------------------------------------------------ + +.. code-block:: easycrypt + + require import Distr. + require import DBool. + require import DInterval. + +``Distr`` -- core distribution theory +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The type ``'a distr`` is built in. The ``Distr`` theory provides: + +- ``mu d E`` -- probability of event ``E`` under distribution ``d``. +- ``mu1 d x`` -- probability of value ``x`` (point mass). +- ``support d x`` -- whether ``x`` has positive probability. +- ``is_lossless d`` -- total probability is exactly 1. +- ``is_full d`` -- every value has positive probability. +- ``is_uniform d`` -- all values in the support have equal + probability. +- ``dmap d f`` -- push-forward: apply ``f`` to samples from ``d``. +- ``dlet d f`` -- monadic bind: sample from ``d``, then from + ``f`` applied to the result. + +``DBool`` -- boolean distributions +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +- ``dbool`` -- fair coin flip (uniform over ``{true, false}``). + +``DInterval`` -- integer distributions +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +- ``[a..b]`` -- uniform distribution over integers from ``a`` to + ``b`` (inclusive). + +``DList`` -- distributions over lists +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +- ``dlist d n`` -- sample ``n`` independent values from ``d``. + +``DProd`` -- product distributions +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +- ``d1 `*` d2`` -- independent product of two distributions. + +``DMap`` -- distribution mapping +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +- ``dmap d f`` (also available in ``Distr``). + +------------------------------------------------------------------------ +Algebra +------------------------------------------------------------------------ + +.. code-block:: easycrypt + + require import Ring. + require import IntDiv. + require import StdOrder. + require import StdBigop. + +``Ring`` -- abstract algebra +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Defines abstract theories for: + +- ``ZModule`` -- additive groups (with ``+``, ``-``, ``0``). +- ``ComRing`` -- commutative rings (adds ``*``, ``1``). +- ``IDomain`` -- integral domains. +- ``Field`` -- fields (adds division). + +These are instantiated by cloning for concrete types like ``int`` and +``real``. The ``ring`` and ``field`` tactics use these instances. + +``IntDiv`` -- integer division +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +- ``(%/)`` -- Euclidean division. +- ``(%%)`` -- Euclidean modulo. +- ``(%|)`` -- divisibility predicate. +- ``gcd``, ``lcm`` -- greatest common divisor, least common multiple. + +``StdOrder`` -- orderings +~~~~~~~~~~~~~~~~~~~~~~~~~ + +Provides abstract ordered types and clones for ``int`` and ``real``: + +- ``IntOrder`` -- ordering lemmas for integers. +- ``RealOrder`` -- ordering lemmas for reals. + +These bring ``<``, ``<=``, ``>``, ``>=`` along with a rich collection +of lemmas (monotonicity, transitivity, etc.). + +``StdBigop`` -- big operators +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Defines summation and products over lists and ranges: + +- ``BIA.bigi`` -- big sum of integers: ``bigi predT f 0 n`` + computes ``f 0 + f 1 + ... + f (n-1)``. +- ``BRA.big`` -- big sum of reals. +- ``BIM.big`` -- big product. + +------------------------------------------------------------------------ +Finite types +------------------------------------------------------------------------ + +.. code-block:: easycrypt + + require import FinType. + require import Finite. + require import Discrete. + +``FinType`` -- enumerable finite types +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The abstract theory ``FinType`` describes types with a finite number +of values. You clone it providing: + +- ``type t`` -- the type. +- ``op enum : t list`` -- a list of all values. + +This gives you the cardinality (``card``) and uniform distribution +over the type (``dunifin``). + +``Finite`` -- general finiteness +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +More general finiteness properties not requiring explicit enumeration. + +``Discrete`` -- discrete types +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Types with a ``witness`` and decidable equality. + +------------------------------------------------------------------------ +Cryptographic theories +------------------------------------------------------------------------ + +.. code-block:: easycrypt + + require import PROM. + require import PKE. + require import Hybrid. + +The standard library includes theories defining standard +cryptographic concepts: + +``PROM`` -- programmable random oracle model +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Provides abstract theories for random oracles that can be cloned +with your specific input/output types. + +``PKE`` -- public-key encryption +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Defines IND-CPA security games for public-key encryption schemes. + +``PKS`` -- public-key signatures +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Defines EUF-CMA security games for signature schemes. + +``Hybrid`` -- hybrid argument +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Provides a generic hybrid argument framework for reducing an +``n``-step distinguishing advantage to a single-step one. + +``Commitment`` -- commitment schemes +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Defines binding and hiding properties for commitment schemes. + +------------------------------------------------------------------------ +Discovering what is available +------------------------------------------------------------------------ + +To find lemmas and definitions in the standard library: + +1. Use ``search`` with a pattern: + + .. code-block:: easycrypt + + search (size (_ ++ _)). + +2. Use ``print`` to inspect a theory: + + .. code-block:: easycrypt + + print theory List. + +3. Use ``locate`` to find where a name is defined: + + .. code-block:: easycrypt + + locate mem. + +4. Read the source files in the ``theories/`` directory of the + EasyCrypt installation. They are well-commented and serve as + the definitive reference.