|
| 1 | +# EasyCrypt — LLM Agent Guide |
| 2 | + |
| 3 | +EasyCrypt is a proof assistant for reasoning about the security of |
| 4 | +cryptographic constructions. It provides support for probabilistic |
| 5 | +computations, program logics (Hoare logic, probabilistic Hoare logic, |
| 6 | +probabilistic relational Hoare logic), and ambient mathematical |
| 7 | +reasoning. |
| 8 | + |
| 9 | +## Using the `llm` command |
| 10 | + |
| 11 | +The `llm` subcommand is designed for non-interactive, LLM-friendly |
| 12 | +batch compilation. It produces no progress bar and no `.eco` cache |
| 13 | +files. |
| 14 | + |
| 15 | +``` |
| 16 | +easycrypt llm [OPTIONS] FILE.ec |
| 17 | +``` |
| 18 | + |
| 19 | +### Options |
| 20 | + |
| 21 | +- `-upto LINE` or `-upto LINE:COL` — Compile up to (but not |
| 22 | + including) the given location, then print the current goal state to |
| 23 | + stdout and exit with code 0. Use this to inspect the proof state at |
| 24 | + a specific point in a file. |
| 25 | + |
| 26 | +- `-lastgoals` — On failure, print the goal state (as it was just |
| 27 | + before the failing command) to stdout, then print the error to |
| 28 | + stderr, and exit with code 1. Use this to understand what the |
| 29 | + failing tactic was supposed to prove. |
| 30 | + |
| 31 | +Standard loader and prover options (`-I`, `-timeout`, `-p`, etc.) are |
| 32 | +also available. |
| 33 | + |
| 34 | +### Output conventions |
| 35 | + |
| 36 | +- **Goals** are printed to **stdout**. |
| 37 | +- **Errors** are printed to **stderr**. |
| 38 | +- **Exit code 0** means success (or `-upto` reached its target). |
| 39 | +- **Exit code 1** means a command failed. |
| 40 | +- If there is no active proof at the point where goals are requested, |
| 41 | + stdout will contain: `No active proof.` |
| 42 | + |
| 43 | +### Workflow for writing and debugging proofs |
| 44 | + |
| 45 | +1. Try to write a pen-and-paper proof first. |
| 46 | + |
| 47 | +2. Write the `.ec` file with your proof attempt. For a large proof, |
| 48 | + write down skeleton and `admit` subgoals first, and then detail |
| 49 | + the proof. |
| 50 | + |
| 51 | +3. Run `easycrypt llm -lastgoals FILE.ec` to check the full file. |
| 52 | + - If it succeeds (exit 0), you are done. |
| 53 | + - If it fails (exit 1), read the error from stderr and the goal |
| 54 | + state from stdout to understand what went wrong. |
| 55 | + |
| 56 | +4. Use `-upto LINE` to inspect the proof state at a specific point |
| 57 | + without running the rest of the file. This is useful for |
| 58 | + incremental proof development. |
| 59 | + |
| 60 | +5. Fix the proof and repeat from step 2. The ultimate proof should |
| 61 | + not contain `admit` or `admitted`. |
| 62 | + |
| 63 | +## EasyCrypt language overview |
| 64 | + |
| 65 | +### File structure |
| 66 | + |
| 67 | +An EasyCrypt file typically begins with `require` and `import` |
| 68 | +statements, followed by type, operator, and module declarations, and |
| 69 | +then lemma statements with their proofs. |
| 70 | + |
| 71 | +``` |
| 72 | +require import AllCore List. |
| 73 | +
|
| 74 | +type key. |
| 75 | +op n : int. |
| 76 | +axiom gt0_n : 0 < n. |
| 77 | +
|
| 78 | +lemma foo : 0 < n + 1. |
| 79 | +proof. smt(gt0_n). qed. |
| 80 | +``` |
| 81 | + |
| 82 | +### Proofs |
| 83 | + |
| 84 | +A proof is delimited by `proof.` and `qed.`. Inside, tactics are |
| 85 | +applied sequentially to transform the goal until it is discharged. |
| 86 | + |
| 87 | +``` |
| 88 | +lemma bar (x : int) : x + 0 = x. |
| 89 | +proof. by ring. qed. |
| 90 | +``` |
| 91 | + |
| 92 | +### Common tactics |
| 93 | + |
| 94 | +<!-- TODO: expand this section with descriptions and examples --> |
| 95 | + |
| 96 | +- `trivial` — solve trivial goals |
| 97 | +- `smt` / `smt(lemmas...)` — call SMT solvers, optionally with hints |
| 98 | +- `auto` — automatic reasoning |
| 99 | +- `split` — split conjunctions |
| 100 | +- `left` / `right` — choose a disjunct |
| 101 | +- `assumption` — close goal from a hypothesis |
| 102 | +- `apply H` — apply a hypothesis or lemma |
| 103 | +- `rewrite H` — rewrite using an equality |
| 104 | +- `have : P` — introduce an intermediate goal |
| 105 | +- `elim` — elimination / induction |
| 106 | +- `case` — case analysis |
| 107 | +- `congr` — congruence |
| 108 | +- `ring` / `field` — algebraic reasoning |
| 109 | +- `proc` — unfold a procedure (program logics) |
| 110 | +- `inline` — inline a procedure call |
| 111 | +- `sp` / `wp` — symbolic execution (forward / backward) |
| 112 | +- `if` — handle conditionals in programs |
| 113 | +- `while I` — handle while loops with invariant `I` |
| 114 | +- `rnd` — handle random sampling |
| 115 | +- `seq N : P` — split a program at statement `N` with mid-condition `P` |
| 116 | +- `conseq` — weaken/strengthen pre/postconditions |
| 117 | +- `byequiv` / `byphoare` — switch between program logics |
| 118 | +- `skip` — skip trivial program steps |
| 119 | +- `sim` — similarity (automatic relational reasoning) |
| 120 | +- `ecall` — external call |
| 121 | + |
| 122 | +### Tactic combinators |
| 123 | + |
| 124 | +- `by tac.` — apply `tac` and require all goals to be closed |
| 125 | +- `tac1; tac2` — sequence |
| 126 | +- `try tac` — try, ignore failure |
| 127 | +- `do tac` / `do N tac` — repeat |
| 128 | +- `[tac1 | tac2 | ...]` — apply different tactics to each subgoal |
| 129 | +- `tac => //.` — apply `tac`, then try `trivial` on generated subgoals |
| 130 | +- `move=> H` / `move=> /H` — introduction and views |
| 131 | + |
| 132 | +### Key libraries |
| 133 | + |
| 134 | +- `AllCore` — re-exports the core libraries (logic, integers, reals, |
| 135 | + lists, etc.) |
| 136 | +- `Distr` — probability distributions |
| 137 | +- `DBool`, `DInterval`, `DList` — specific distributions |
| 138 | +- `FSet`, `FMap` — finite sets and maps |
| 139 | +- `SmtMap` — maps with SMT support |
| 140 | +- `PROM` — programmable/lazy random oracles |
| 141 | + |
| 142 | +### Guidelines |
| 143 | + |
| 144 | +* Use SMT solver only in direct mode (smt() or /#) on simple goals (arithmetic goals, pure logical goals). |
| 145 | + |
| 146 | +* Refrain from unfolding operator definitions unless necessary. |
| 147 | + If you need more properties on an operator, state this property in a dedicated lemma, |
| 148 | + but avoid unfolding definitions in higher level proofs. |
| 149 | + |
0 commit comments