[Easycrypt-club] Questions sur la langue EasyCrypt

Santiago Zanella szanella at gmail.com
Lun 30 Avr 15:02:04 CEST 2012


Hi Cathy,

Please note that the official language of this mailing-list is English,
so do not be afraid of posting your messages in English.


I can give you a rough description of what most used tactics do:

* call [<rel-exp>]

Applies the two-sided Relational Hoare Logic rule for procedure
calls. The argument is a relational invariant and is optional. When
present, EasyCrypt will try to find a matching previously proven
'equiv' statement; if none is found, it will try to prove that the
invariant holds. If the argument is omitted, it is assumed that the
invariant is equality over all common global variables of the two
games in the judgment.


* inline[{1|2}] at i,..,j
* inline[{1|2}] P_1,..,P_j

Inlines the definition of a concrete procedure. In the first variant,
a list of the procedure calls to be inlined is specified by giving the
positions where they appear in the game(s). In the second variant, a
list of procedure names is given and all the corresponding calls are
inlined. Optionally, the transformation can be applied only on the
left-hand side game (inline{1}) or only on the right-hand side game
(inline{2}).


* asgn

Applies the two-sided RHL rule for deterministic assignments

  c1 ~ c2 : P ==> Q[x{1}/e1,y{2}/e2]
======================================
 c1; x <- e1 ~ c2; y <- e2 : P ==> Q


* rnd{1|2}

Applies the one-sided rule for random assignments

 c1 ~ c2 : P ==> forall a:A, Q[x{1}/a]
=======================================
      c1; x <$- A ~ c2 : P ==> Q


* rnd
* rnd (f)
* rnd (f),(finv)

Apply the two-sided RHL rule for random assignments

 c1 ~ c2 : P ==> f is 1-1 /\ forall a:A, Q[x1/f(a), x2/a]
==========================================================
        c1; x1 <$- A ~ c2; x2 <$-B : P ==> Q

When no argument is given, f is assumed to be the identity function.
When just one argument is given, f is an expression interpreted on the
state of the second program and must denote an idempotent
function. When two arguments are given, they must denote functions
that are inverse of each other.


* if

Applies the two-sided RHL rule for conditionals

P => e1{1} = e2{2}
c1  ~ c2  : P /\  e1{1} ==> Q
c1' ~ c2' : P /\ !e1{1} ==> Q
===========================================================
 if e1 then c1 else c1' ~ if e2 then c2 else c2' : P ==> Q


* while{1|2} [at n] : <rel-exp>

Applies the two-sided RHL rule for while loops, using the relational
expression given as argument as loop invariant.


* while [at n] : <rel-exp> : <variant> , <bound>

Applies the one-sided RHL rule for while loops, using <rel-exp> as
loop invariant, <variant> as the increasing variant and <bound> as the
upper bound. The variant and the bound are used to check termination.


* unroll[{1|2}] [at n]

Unrolls the first iteration of a while loop (at position n, 1 by
default).


* strengthen[{1|2}] [at n] : <rel-exp>

Splits a while loop (at position n, 1 by default) into two loops, i.e.
it replaces

 while e do c

with

 (while (e /\ <rel_exp>) do c); while e do c


* app m n <rel-exp>

Applies the RHL rule for sequential composition:

c1 ~ c2 : P ==> Q     c1' ~ c2' : Q ==> R
=========================================
      c1; c1' ~ c2; c2' : P ==> R

It defines c1 as the first m instructions of the program on the
left-hand side and c2 as the first n instructions of the program on
the right-hand side.


* condt[{1|2}] [at n]
* condf[{1|2}] [at n]

Collapses a conditional instruction (at position n, 1 by default) when
the branch taken can be predicted.


* case[{1|2}]: <bool-exp>

Does a case analysis on the value of the Boolean expression given as
argument, resulting in two sub-goals.


* swap[{1|2}] n

Pushes the first instruction n positions down if n is positive.
Pushes the last instruction n positions up if n is
negative. Dependencies are checked to verify the transformation is
semantics-preserving.


* swap[{1|2}] [i-j] n

Pushes the block of instructions on lines i-j n positions down if n is
positive, or n positions up if n is negative. Dependencies are checked
to verify this is admissible.


* derandomize[{1|2}]

Hoists random assignments up-front when this is possible.


* wp

Computes the relational weakest-precondition of deterministic, loop
and procedure-call free program fragments (i.e. deterministic
assignments and conditionals). For example, if c1' and c2' fit in this
fragment, applying this tactic amounts to apply the rule

   c1 ~ c2 : P ==> wp(c1',c2',Q)
====================================
   c1; c1' ~ c2; c2' : P ==> Q


* let[{1|2}] [at n] <var> : <type> = <exp>

Inserts an auxiliary assignment (at position n, 1 by default).


* admit

Admits the current goal without proof.


* expand p_1,..,p_n

Expands the definition of predicates p_1,..,p_n in the current goal.


* apply[{1|2}]: <spec> (e1,..,e2)

Applies a probabilistic operator specification previously introduced
using the 'spec' directive.


Some tactics implement heuristics and strategies in order to solve or
simplify a goal:

* trivial

Combines wp and rnd to simplify the goal. It tries to match random
assignments in both programs applying the two-sided rule; if this
fails it will apply the one-side rule.


* simpl

Computes the weakest precondition of the deterministic, loop-free
suffix of the games in the judgment. It then simplifies the resulting
post-condition by eliminating absurd and trivial cases.


* auto [<rel-exp>]

Computes the weakest precondition of the deterministic, loop-free
suffix of the games in the judgment. When encountering procedure
calls, it looks for a matching proven 'equiv' statement; if none is
found it tries to prove one using the optional <rel-exp> argument as
invariant. It stops when it encounters a random assignment.


EasyCrypt has a simple language of tacticals that can be used to build
more complex tactics from basic tactics. The following is brief a
description of the tactic language of EasyCrypt:


* idtac

Does nothing.


* <tactic_1> ; <tactic_2>

Applies <tactic_1>, then <tactic_2>.


* <tactic>; [ <tactic_1> | .. | <tactic_n>]

Applies <tactic>, then applies <tactic_i> to the ith-subgoal.


* *<tactic>

Prefixing any tactic expression with '*' results in the tactic being
repeatedly applied until it fails.


* !n<tactic>

Repeats the tactic given as argument n times.


* try <tactic>

Tries to apply the tactic given as argument, if it fails, it catches
the error.


There is preliminary support in EasyCrypt for handling an approximate
variant of RHL, which can be used to reason about statistical distance
and differential privacy. Note that some of the tactics described
above have approximate variants that usually take extra arguments. For
instance, the tactic 'app' has an approximate variant whose extra
arguments are used to specify the 'skew' and the 'slack'. The
following commands can be used to switch between the approximate and
exact variants of RHL during a proof:

* pRHL

Translates an approximate goal into the standard variant of RHL, when
the skew is 1 and the slack is 0.

* apRHL

Translates a pRHL goal into its approximate form, with skew 1 and
slack 0.


Hope this helps in the meantime, while we work on a proper documentation.

Best Regards,
--Santiago



More information about the Easycrypt-club mailing list