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
