https://github.com/EasyCrypt/easycrypt
Raw File
Tip revision: 0659058a2f037906614c734205bc53d3d85d8919 authored by Pierre-Yves Strub on 05 February 2020, 15:19 UTC
Merge branch '1.0' into deploy-momemtum
Tip revision: 0659058
note.txt

msem : code -> mem -> mem distr
dsem : code -> mem distr -> mem distr

munit : 'a -> 'a distr.
axiom munit_def : $[f | munit a] = f a.

mlet : 'a distr -> ('a -> 'b distr) -> 'b distr.

axiom mlet_def : $[f | mlet d F] = $[fun a => $[f | F a] | d]

dsem c mu = mlet mu (mem c)
msem c m  = dsem (munit a)

[ P ] c {phi}
{$[1_P] = 1%r} c {phi}


(* -------------------------------------------------------------- *)
muf (fun x => b2r (! f)) d = 0 --> $@[x: f | mu]
si x : memory alors active_mem x
si mu : active_distr alors     --> $@[x: f]
muf (fun x => f) d = 0         --> $[x: f | mu]
si x : memory alors active_mem x
si mu : active_distr alors     --> $[x: f]




il faudrait avoir des variables de range comme ca on peut faire ce que l'on veut.
Il y a les memoires globales
memoire = memoire global + record 

type upd {
  var -> form
  glob -> form
}

upd_mem : form -> upd -> form
|- m : memory mt    ||- upd : mt
---------------------------------
|- upd_mem m upd : memory mt

get_mem : form -> pvar -> form
|- m : memory mt   mt |- x : t
------------------------------
|- get_mem m x : t


Remarque on a besoin de faire deux type de substitution de variables:
Remplacement d'une variable:
  m[x := f]     pour le wp et random,

Regles de simplification:
 m[x := f][x]      --> f
 m[x := f][y]      --> m[y]               if x <> y
 m[x := f][glob A] --> m[glob A]          if disjoint glob A x.

 m[x := f][y:=f']  --> m[y:= f'][x:= f]   if x <> y
 m[x := f][x:=f']  --> m[x:=f']

Remplacement d'un ensemble de variables par variables universellement 
  quantifiees:
m [x1,....,xn, glob A1, glob An ::= m']

Regles de simplification:
 m[vars ::= m'][x]      --> m'[x]             if x in vars
 m[vars ::= m'][x]      --> m[x]              if x not in vars
 m[vars ::= m'][glob A] --> m'[glob A]        if glob A included in vars
 m[vars ::= m'][glob A] --> m[glob A]         if glob A disjoint vars
 
 m[vars ::= m'][glob A] --> m[vars' := m'][glob A] 
             where vars' { x(resp glob B) in vars | 
                            not glob A disjoint x(resp glob) }
 
Explanation on x in vars = x1, ..., xn, glob A1, ... glob An
  - x in xi then x in vars
  - x not in xi and x not in glob Ai then x not in vars
  - glob A included in vars if A in Ai
  - glob A disjoint vars if A can not read/write xi and glob Ai

  
 

 













On peut exprimer qu'une formule est invariante par upd
forall (g:glob A) (m: mt mem), P m => P (m[glob A <- g])
Idem pour les relations:
forall (g:glob A) (m1: mt1 mem) (m2:mt2 mem), R m1 m2 => 
           R (m1[glob A <- g]) (m2[glob A <- g])
 
Regle de reduction:
x{m[x<-t; other]} -> t si other disjoint x

x{m[upd]} -> x{m[remove x upd]}

remove x upd = 
  upd [glob A 




clone 
  with theory T1 <- T2
  with module M1 <- M2
  with lemma l1 <- l2
  rename regexp by regexp 

clone include T1 as T2
pour faciliter les clones futurs.
 
rename : 
  renomage des lemmes, operateurs, types, modules, variables globales,
  variables locales.

c'est quoi : 
  { 'a support | wf_support<:'a> }
back to top