# Stage de Théo Losekoot

## Biblio du M2SIF

* Date 15/12 soumission d'un résumé
* 5(0)% of bibliographic references must by cited and section/subsection titles should be almost definitive.
* 22/01/21
* Rapport prêt à 75%
* 27/01/21
* Vidéo de 15 minutes
* 12/02/21
* Fini
* Contenu
* 10 to 15 pages (in total, including bibliographic references, annexes and not including the cover page, table of contents)

Lien des consignes :
https://gitlab.inria.fr/grossamb/m2sif/-/wikis/Bibliographic-study-(BIBL)

Lectures:
1. Thèse de Timothée (au 19/11/20, chapitre 1 et presque 2 lus)
2.

### Plan

1. Intro (1 à 2 pages)
1. Qu'est-ce que la verif formelle (1 paragraphe sur la vérification automatique)
2. Vérif automatique par langages réguliers (1 autre paragraphe) [ICFP]
3. Limites -> on n'a pas de relations
2. Préliminaires (< 2 pages?)
1. Réécriture [Référence Réécriture Baader/Nipkow "Rewriting and all that"]
2. Automates d'arbres [Tata]
3. Relations régulières (2 types de convolution standard/full) [Automatic relations KN95 + Tata]
3. État de l'art (9 pages)
1. Vérif automatique par langages réguliers [ICFP]
2. Principe ICE + learner + teacher (lire le papier) [Champion, T. Chiba etc.]
3. Principe ICE pour relations régulières (standard convolutions) [Thèse]
4. Objectif de la seconde partie du stage (après la bibl) (~1 page)
ICE + learner + teacher ... avec des full convolutions.
5. Biblio (1 page)

### Citations complémentaires ###

* type annotations. [LiquidTypes Ranjit Jahla] [Fstar*] (partie 3.1)
* [MKU15] (partie 3.3) Y. Matsumoto, N. Kobayashi, and H. Unno. Automata-based abstraction for automated verification of higher-order tree-processing programs. In X. Feng and S. Park, editors, Programming Languages and Systems, pages 295–312, Cham, 2015. Springer International Publishing.

### Explications ###

$a \cup b$

$R^*(I) \subseteq L \subseteq Prop$

[Thèse de Valérie Murat] Lattice Tree Automata (LTA) (2013 pas automatique)
$cons(q, ql) \rightarrow ql$
$[0;10] \rightarrow q$
$nil \rightarrow ql$

Mettre au point un système de type raffiné (e.g. Liquid Types/celui de Timothée) qui utiliserait des langages reconnus par un LTA (?) (comme langage d'entrée et intermédiaire)

$t: q$ veut dire $cons(x,l) : \{x >10 \wedge l \in L(A,q) \}$

$f(x : ql)$ le $ql$ est un état de LTA.

--

$F\: x\: y \rightarrow c (x\: a)\: (y\: b)$

### Ordre de lecture pertinent ###

pas vraiment d'ordre finalement - ne pas être strict:
- Matsumoto MKU2015 *
- Thèse de timothée, 6.4 *
- Example 5.3.8. "Consider again the TRS defined by" -- p. 110
- lire intros sections 4 et 5 (de la thèse) *
- [fstar](https://www.fstar-lang.org/tutorial) regarder 6(.1)
- Automatic relations KN95
- Lire Genet2018verifying *
- Liquid Types *
- TATA sur les convolutions. Oui!
- ICE Learner teacher Champion 2020 (après la thèse)

### Rendez-vous ###

- lundi 04/01/2021 10h - OK
- mardi 12/01/2021 10h - OK
- mardi 19/01/2021 10h - OK
- lundi 25/01/2021 10h - OK
- mardi 26/01/2021 10h - OK
- lundi 01/02/2021 10h - OUPS
- lundi 01/02/2021 16h - OK

liste d'entiers pairs puis impairs ?:
$ilist = \{True ; \langle i:int, \{\_ \mid w : \_, w\%2 \geq i\%2 \} \rangle\}$

## Vidéo

### Motivations
ce sujet
#### Prouver des propriétés sur des programmes

Why3, F*, Liquid Types etc. Coq/(Isabelle/HOL)

#### ... automatiquement

On commence à savoir le faire sur des propriétés
numérique et relationnelles ou structurelles mais non relationnelles.

Ex. double (?)

#### Relationnelles

On veut des propriétés relationnelles et structurelles

#### Méthode de timothée
* Illustrer le type de propriétés auxquelles on s'intéresse
* Principe de résolution... utilisation des SMT pour découvrir l'automate (?)
* q1=q2 --> q3!=q4
* q5!=q6
* ...

Ex double?

#### Objectif du stage
étendre aux propriétés relationnelles

double n >= n

### Autres ###
$let f n = (fun x -> x + n)$

$f(\underline{n}) \rightarrow @(ff, \underline{n})$ et $@(@(ff,\underline{n}), \underline{x}) \rightarrow +(\underline{n},\underline{x})$ ?
$@(@(ff,\underline{n}), \underline{x}) \rightarrow *(\underline{n},\underline{x})$

L'opération qui définit $ff$ pour remplacer la fonction anonyme = "Lambda-lifting".

### différents types de model-checking ###

* Model-checking (I fini, O fini, R*(I) fini)
* Regular Model-checking (I régulier, O régulier, R*(I) régulier)
* Abstrat Regular Model-checking (I Régulier, O Régulier, et on construit des Sur-approx régulières de R*(I)) (La propriété est prouvée si l'approx est <= O)
* Abstrat Regular Tree Model-checking (I Langage d'arbres Régulier, O langage d'arbres Régulier, et on construit des Sur-approx régulières de R*(I)) (La propriété est prouvée si l'approx est <= O)
* Bouajjani: R n'est pas un TRS mais un tree transducer.

Jerôme Leroux : Travaille à reconnaître des relations régulières avec les automates, mais ce sont des relations sur les chaines de caractères. à voir.

GADT

type empty_t = Empty_t;;
type not_empty_t = Not_empty_t;;
type ('a, 'b) mlist =
  | Nil : (empty_t, 'b) mlist
  | Cons : ('b * ('a, 'b) mlist) -> (not_empty_t, 'b) mlist;;

let x= Nil;;
let l= Cons(1, Cons(2, Cons(3, Empty)));;


(* On laisse un _ dans le type de droite pour voir s'il peut l'inférer *)

let rec append : type a1 a2 . ((a1, 'b) mlist) -> ((a2, 'b) mlist) -> _ = fun l1 l2 ->
  match l1 with
  | Nil -> l2
  | Cons(x,y) -> Cons(x, append y l2);;

(* Dans la mesure où les appels récursifs se feront sur des types différents on doit déclarer les 
   variables de type a1 a2 au préalable. Le type de sorti on le laisse inconnu. *)

Déroulage exemple:

R=

double(0) -> 0
double(s(X)) -> s(s(double(X)))

I=

double(qnat) -> qf
0 -> qnat
s(qnat) -> qnat

O =

0 -> qe
s(qe) -> qo
s(qo) -> qe

L(A0)= {double(0)}

double(q0) -> qf0
0 -> q0

1. On le complète par R (on veut que l'automate reconnaisse tous les termes et leurs descendants pas réécriture dans le même état)

2. Existe-t-il un terme (irréductible par R) de L(A0) qui sort de O?
   Ici le seul terme est 0 qui est contenu dans O. OK.
   
3. On tente de minimiser le nombre d'états de l'automate en considérant toutes les fusions d'état
   possibles mais en respectant O (SMT)
   
   q0=qf0
   

double(qf0) -> qf0
0 -> qf0

4. Est-ce que l'automate reconnaît tous les états initiaux?

    Non ... il ne reconnaît pas double(s(0))
    
L(A1)={double(0),double(s(0))}

double(q0) -> qf0
0 -> q0
s(q0) -> q1
double(q1) -> qf0

1. On le complète par R (on veut que l'automate reconnaisse tous les termes et leurs descendants pas réécriture dans le même état)

q0 -> qf0
s(qf0) -> q3 // car double(s(0)) -> s(s(double(0)))
s(q3) -> q4
q4 -> qf0

Cet automate reconnaît {double(0), double(s(0)), s(s(double(0))), s(s(0)), 0}

s(s(0)) -> s(s(q0)) -> s(s(qf0)) -> s(q3) -> q4 -> qf0

2. Existe-t-il un terme (irréductible par R) de L(A0) qui sort de O?
   Ici les deux seuls termes sont 0 et s(s(0)) qui sont contenus dans O. OK.
   
3. On tente de minimiser le nombre d'états de l'automate en considérant toutes les fusions d'état
   possibles, mais en respectant O (SMT)
   
   q4=qf0
   q1=q3
   q0=qf0
   
   double(q0) -> qf0

0 -> qf0
s(qf0) -> q1
double(qf0) -> qf0
double(q1) -> qf0
s(qf0) -> q1
s(q1) -> qf0

0 -> 0#
s(0#) -> 1#
double(1#) -> 0#
double(0#) -> 0#
s(0#) -> 1#
s(1#) -> 0#

4. Est-ce que l'automate reconnaît tous les états initiaux?

    Oui ... il reconnaît pas double(s*(0))
    
5. Est-ce qu'il est R-clos? Oui aussi.
    
    sur un exemple: double(s(s(0))) ->*R s(s(s(s(0)))) et on a s(s(s(s(0)))) reconnu.
    
    
   ------
   
   Exemple fonctionnement de l'algo modulaire :

1.
sorted(sort l) -> {true#,false#}

sorted(X:L) -> {true#, false#} ?
L= {sortedList#,unsorted#}

sorted(sortedList#) -> true#
sorted(unsorted#) -> false#

2.
sort(l:list#) : {sortedList#, unsorted#}

sort(list#) -> sortedList#

f : qtrue -> qtrue
f : qfalse -> qfalse
f : qbool -> qbool

Ce qu'il cherche c'est "un" type pour even tq:

L1 = qeven
L2 = qodd 

even(x:qeven) -> qtrue
even(x:qodd) -> qfalse

even(x:qnat) -> qbool

{nat} = {L1,L2} ??

Exemple 5.9

xor(f(X:nat#),Y:bool#) -> {true#,false#}

1.
xor(X,Y) -> {true#,false#}

xor({true#,false#},{true#,false#}) -> {true#,false#}

ff(x,true) -> true
ff(x,false) -> false

ff({bool#},{true#,false#}) -> {true#,false#}