https://github.com/EasyCrypt/easycrypt
Raw File
Tip revision: a79f9aeb6de046ca12210d26317fab59c175d0dd authored by Pierre-Yves Strub on 08 July 2014, 09:43 UTC
Fix bug w.r.t. _tools presence detection.
Tip revision: a79f9ae
TODO.txt
Discussion la semaine prochaine:
  - Pressentation du code (important pour les developpeurs)
  - Reviews de theories
  - Reviews des tactics elementaires
  - Reviews des tactics utilisateurs

Verifier les fonction add dans ecEnv.

Printer :

Parser  : 
+  introduire une notation looslessA A.f : 
    (forall (O<:O),  bd_hoare [O.hashA : true ==> true] [=] [1%r] => 
      bd_hoare [A(O).a : true ==> true] [=] [1%r]).


Message d'erreur:
(* rewrite (Set.add_mem F2.xs{m2} x{m2} RO.logA{m2}). *)
(* FIXME error message *)  
 


* Pierre-Yves

- reprendre la partie module -> finir la partie typage
- pretty-printing de l'AST typé
- noeud de meta-info dans les AST typés
- local predicates / operators
- ec échoue sur une erreur système lorsque why3 est configuré pour 0 prouveur.

* Benjamin

tactic :

 add tactic like : intros \ for intros H;clear H.

 Deplacer le module PV et PVM dans un fichier separer avant (ecLogic.ml)
 Permet de faire subst avec des pv.

  + tactic phl/prhl 
    - eqobs_in
    - not_modify
    - hoare -> equiv
    - derandomize
    - rename trivial into prover 
    - use trivial for more sofisticated tactic:
          simplify; intuition; subst; try split;prover  
    - subst should also works for program variable.

  + tactic
    - set 
    - apply avec instanciation automatique +
      apply f   
    - notation apply recursive

  + Why3 : 
    - partage des events (* ie. function annonyme *)
    - netoyage des tasks 
    - base de hint  (* Voir avec francois *)
    - triggers      (* Voir avec francois *)

clone : 
  + finir les toutes les instanciations possibles


* Parsing:
- Nom long pour les operateurs infix, 

* Pretty:
- Affichage des noms long ou cours, ty instance

* TODO
- chemins privés (attendre la fin des modules)

- réfléchir sur le pb d'instanciation de modules
  (=> hypothèses sur adversaire - e.g. pour up-to-bad)
- arbre de preuve + contexte dynamique de preuve
- batterie de tests
- mot-clef "use" + nettoyage de task
- raffinements
- diff. for modules


Discussion :
  semantique de hoare f : p => q 
    forall m, p m => range q [f m]
  ou avoir simplement le range.

  rajouter le assume il y a une semantique facile pour le justifier.

    
  Nomage des variables (path) :
    Variables de programe : 
      Globals            :  th_path :: mod_path :: var_id
      Parameters, Locals :  th_path :: mod_path :: fun_id :: var_id

    Locals (let, forall, exists) : var_id.

  EcEnv doit assurer pas de clach de noms long :
    Variables de programe :
       pas deux variables avec le meme qsymbol 
    Locals : pas de contrainte sur le symbol (seulement des idents different)

    Operateurs : pas deux operateurs avec la meme arite 
                            (on peut etre moin restrictif, type non unifiable)
                 avec le meme qsymbol.
    Type : pas deux type avec le meme qsymbol.

    Module :  pas deux type avec le meme qsymbol
      Question : c'est quoi le path d'un parametre de module :
             F (A:T) = { }
             path de F :: A_id
           
    Module type :  pas deux type avec le meme qsymbol

    On doit pas avoir de theory et de module avec la meme qsymbol ? 
       theory T.
        theory M.
           cnst x : int.
        end M.
        module M = {
           var x : int.
        }.
       end T.  



*** Note de discussion

i_inuse : LvMap `Read ok mais aussi `Write

*** 

 - Les types sont étendus avec un constructeur unaire Tglob.  Tglob(M)
   représente le types des variables globales (en tant que n-uplet) de
   M. Il est incertain si Tglob(M) ne contient que le types des
   variables non connues de M ou non.

 - Les formules sont étendues avec un nouveau constructeur
   représentant les variables globales d'un module dans une mémoire
   donnée:

     Cglob : module x mem -> form

 - Faire l'extension de la substitution en conséquence.

***

 - 

*** upto rule

* Preliminary definitions :
  + DISTR 
    distr (A:Type) := (A -> [0,1]) -> [0,1]

  + SEM : notation [c] m 
    sem (s:stmt) (m:mem) : distr mem 
 
  + RANGE
    range A (P : A -> Prop) (d:distr A) : Prop := 
       forall (f:A -> [0,1]),  (forall a, P a -> f a = 0) => d f = 0

  + LOSSLESS 
    lossless A (d:distr A) : Prop := d 1_true = 1

  + RANGEB : notation { P } c { Q } = 1 
                            (* Particular case of Cesar implementation *)
    rangeb : (P : mem -> Prop) (c:stmt) (Q:mem -> Prop) : Prop := 
       forall m, P m => [c] m 1_Q = 1

    Remark 1 : range P ([c] m) + lossless ([c] m) => rangeb P c 

  + LIFT 
    lift (R:A -> B -> Prop) (d1:distr A) (d2:distr B) :=
      exists d:distr (A * B), 
        condition 1 : d o Fst = d1
        condition 2 : d o Snd = d2
        condition 3 : range R d   (abusing notation the relation R can be see 
                                  as a predicate over (A * B) )
  + EQUIV :
    equiv (P:mem -> mem -> Prop) (c1 c2:stmt) (Q:mem -> mem -> Prop) :=
       forall m1 m2, P m1 m2 => lift Q ([c1] m1) ([c2] m2)


* Usefull Lemmas :
  + lemma mu_cte :
    d (Fcte r) = r * d 1_true
    if lossless d, d (Fcte r) = r

  + lemma 1 : 
    {P} c {Q} = 1  => forall m, P m => [c] m E = [c] m (E_{|Q})
    where E_{|Q} = fun m' -> 1_Q m' * E m'  
 
  + lemma 2 : 
      {P} c {Q} = 1 => forall m, P m => [c] m 1_true = 1
     Proof. trivial, since Q => true

  + lemma 3 :
     H1 : {P1} c1 {Q1} = 1                  =>
     H2 : {P2} c2 {Q2} = 1                  =>
     H3 : (forall m1 m2, P m1 m2 => P1 m1)  =>
     H4 : (forall m1 m2, P m1 m2 => P2 m2)  =>
     H5 : (forall m1 m2, Q1 m1 => Q2 m2 => Q m1 m2) =>

     forall m1 m2, 
        H6 : P m1 m2 =>
        lift Q ([c1]m1) ([c2]m2)
    Proof.
      take d = 
        Mlet ([c1] m1) 
          (fun m1' -> Mlet ([c2] m2) 
             (fun m2' -> (m1', m2'))) 

      condition 1 : d o Fst == [c1] m1 
        forall E,
          (d o Fst) E = 
          [c1] m1 (fun m1' -> [c2] m2 (fun m2' -> E (fst (m1',m2')))) =
          [c1] m1 (fun m1' -> [c2] m2 (E m1')) =      
          (* mu_cst  *)
          [c1] m1 (fun m1' -> E m1' * [c2] m2 True) = 
          (* lemma 2 + H2 + H3 + H6 *)
          [c1] m1 (fun m1' -> E m1') = 
          [c1] m1 E (* CQFD *)

      condition 2 : d o Snd = [c2] m2
         same as 1 since 
         d == Mlet ([c2] m2)
                (fun m2' -> Mlet ([c1] m1) (fun m1' -> (m1',m2'))) 

      condition 3 (range (fun (m1,m2) -> Q m1 m2) d) :
         - assume H7 : (forall m1' m2', Q m1' m2' => f (m1', m2') = 0)
         we should prove d f = 0
         d f = 
         [c1] m1 (fun m1' -> [c2] m2 (fun m2' -> f (m1', m2')) =
                (* by lemma 1 + H3 + H6 *)
         [c1] m1 (fun m1' -> 1_Q1 m1' * [c2] m2 (fun m2' -> f (m1',m2'))) =
                (* mu_cte *)
         [c1] m1 (fun m1' -> [c2] m2 (fun m2' -> 1_Q1 m1' * f (m1', m2'))) =
                (* by lemma 1 + H4 + H6 *)
         [c1] m1 (fun m1' -> [c2] m2 
                     (fun m2' -> 1_Q1 m1' * 1_Q2 m2' * f (m1',m2'))) =
                (* by next remark *)                 
         [c1] m1 (fun m1' -> [c2] m2 (Fcte 0)) = 
         [c1] m1 (fun m1' -> 0) = [c1] m1 (Fcte 0) =
         0 (* CQFD *)
        next_remark : 
          forall m1' m2',
             1_Q1 m1' * 1_Q2 m2' * f (m1',m2') = 0
         if !(Q1 m1' /\ Q2 m2') then !Q1 m1' \/ !Q2  m2' and trivial
         else by H5 + H7 

   
Now we try to prove the upto bad rule :

  P,Q : sided formulas depending only of global variables disjoint of the 
         adversary memory.
  Bad a formula depending only of global variables disjoint of the adversary 
  memory.
  ( i.e. the adversary can not write global variables of P, Q and Bad )

  condition 1 : o1_i ~ o2_i : 
     !Bad{2} /\ ={args} /\ (glob A){1) = (glob A){2} /\ P ==> 
     if Bad{2} then Q
     else (={res} /\ (glob A){1) = (glob A){2} /\ P )

  condition 2 : forall m2, Bad m2 => { Q(_,m2) } o1_i { Q(_,m2) }
           where Q(_,m2) means fun m1 -> Q m1 m2.
  condition 3 : forall m1, { Bad /\ Q m1 } o2_i { Bad /\ Q m1 } 
         

  condition 4 : forall m, lossless ([o1_i] m)

  condition 5 : forall m, lossless ([o2_i] m)

  condition 5 : forall o, 
      (forall m,  lossless ([o] m)) =>
      forall m, lossless ([A.f_{o}] m)
----------------------------------------------------------------------
  A.f_{o1} ~ A.f{o2} : 
     if Bad{2} then Q
     else (={params} /\ (glob A){1) = (glob A){2} /\ P ) ==> 
     if Bad{2} then Q
     else (={res} /\ (glob A){1) = (glob A){2} /\ P )

Proof by induction on the adversary statement (more precisely 
by induction on the well formed adversary predicate)
We prove :
   s(o1) ~ s(o2) : 
     if Bad{2} then Q 
     else ( (mem A){1) = (mem A){2} /\ P ) 
     ==>
     if Bad{2} then Q 
     else ( (mem A){1) = (mem A){2} /\ P )

Instead of using equiv we use lift :
let INV = if Bad{2} then Q else ( (mem A){1) = (mem A){2} /\ P )

  forall s m1 m2,
     INV m1 m2 =>
     lossless ([s_{o1}] m1) =>
     lossless ([s_{o2}] m2) =>
     lift INV ([s(o1)] m1) ([s(o1)] m2)

By induction on s.
Each case start by a case analysing on Bad m2
if Bad m2 is true the we use the same proof that for lemma 3
we need to prove 
    range ([s_{o1}] m1) Q(_, m2)
and range ([s_{o2}] m2) (Q m1)
This is easy because s can not write the variable of Q

Now we have to do all case knowing !(Bad m2) :
We have 
  (1)   (mem A) m1 = (mem A) m2 and 
  (2)   P m1 m2
+ case s := x = e trivial since
  x does not affect P, and e m1 = e m2 by (1)
+ case s := i;s'
  We apply the induction hypothesis on i 
  First difficulty prove that lossless ([i_{oj}] mj) 
   (if not then ([s_{oj}] mj) is not lossless,  absurd)
  Then we apply the induction hypothesis on s' 
  remark that the initial memory mj' given to s' are "reachable" from i, mj
  and so if !lossless ([s'_{oj}] mj') then !lossless ([s_{oj}] mj)
+ case s := if e then s' else s''
  e m1 = e m2 by 1 and so both statement take the same branch and
  we conclude by induction hypothesis.
+ case s := while e do s' 
  should be a mixte of case if and cons.
  The difficulty is to prove that s' is lossless for each "reachable" state
  of the loop.
+ case s := x := f(e)  
  two possibility : 
   1/ f is an oracle, trivial by hypothesis
   2/ f is an adversary function by induction hypothesis

  





  



     





back to top