Integration of Jacques-Henri Jourdan's verified parser.

(Merge of branch newparser.)


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2469 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

11 files changed, 3138 insertions, 0 deletions

diff --git a/cparser/validator/Alphabet.v b/cparser/validator/Alphabet.v
new file mode 100644
index 0000000..f47f136
--- /dev/null
+++ b/cparser/validator/Alphabet.v
@@ -0,0 +1,321 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Jacques-Henri Jourdan, INRIA Paris-Rocquencourt            *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+Require Import Int31.
+Require Import Cyclic31.
+Require Import Omega.
+Require Import List.
+Require Import Syntax.
+Require Import Relations.
+Require Import RelationClasses.
+
+Local Obligation Tactic := intros.
+
+(** A comparable type is equiped with a [compare] function, that define an order
+   relation. **)
+Class Comparable (A:Type) := {
+  compare : A -> A -> comparison;
+  compare_antisym : forall x y, CompOpp (compare x y) = compare y x;
+  compare_trans :  forall x y z c,
+    (compare x y) = c -> (compare y z) = c -> (compare x z) = c
+}.
+
+Theorem compare_refl {A:Type} (C: Comparable A) :
+  forall x, compare x x = Eq.
+Proof.
+intros.
+pose proof (compare_antisym x x).
+destruct (compare x x); intuition; try discriminate.
+Qed.
+
+(** The corresponding order is a strict order. **)
+Definition comparableLt {A:Type} (C: Comparable A) : relation A :=
+  fun x y => compare x y = Lt.
+
+Instance ComparableLtStrictOrder {A:Type} (C: Comparable A) :
+  StrictOrder (comparableLt C).
+Proof.
+apply Build_StrictOrder.
+unfold Irreflexive, Reflexive, complement, comparableLt.
+intros.
+pose proof H.
+rewrite <- compare_antisym in H.
+rewrite H0 in H.
+discriminate H.
+unfold Transitive, comparableLt.
+intros x y z.
+apply compare_trans.
+Qed.
+
+(** nat is comparable. **)
+Program Instance natComparable : Comparable nat :=
+  { compare := nat_compare }.
+Next Obligation.
+symmetry.
+destruct (nat_compare x y)  as [] eqn:?.
+rewrite nat_compare_eq_iff in Heqc.
+destruct Heqc.
+rewrite nat_compare_eq_iff.
+trivial.
+rewrite <- nat_compare_lt in *.
+rewrite <- nat_compare_gt in *.
+trivial.
+rewrite <- nat_compare_lt in *.
+rewrite <- nat_compare_gt in *.
+trivial.
+Qed.
+Next Obligation.
+destruct c.
+rewrite nat_compare_eq_iff in *; destruct H; assumption.
+rewrite <- nat_compare_lt in *.
+apply (lt_trans _ _ _ H H0).
+rewrite <- nat_compare_gt in *.
+apply (gt_trans _ _ _ H H0).
+Qed.
+
+(** A pair of comparable is comparable. **)
+Program Instance PairComparable {A:Type} (CA:Comparable A) {B:Type} (CB:Comparable B) :
+  Comparable (A*B) :=
+  { compare := fun x y =>
+      let (xa, xb) := x in let (ya, yb) := y in
+      match compare xa ya return comparison with
+        | Eq => compare xb yb
+        | x => x
+      end }.
+Next Obligation.
+destruct x, y.
+rewrite <- (compare_antisym a a0).
+rewrite <- (compare_antisym b b0).
+destruct (compare a a0); intuition.
+Qed.
+Next Obligation.
+destruct x, y, z.
+destruct (compare a a0) as [] eqn:?, (compare a0 a1) as [] eqn:?;
+try (rewrite <- H0 in H; discriminate);
+try (destruct (compare a a1) as [] eqn:?;
+  try (rewrite <- compare_antisym in Heqc0;
+         rewrite CompOpp_iff in Heqc0;
+         rewrite (compare_trans _ _ _  _ Heqc0 Heqc2) in Heqc1;
+         discriminate);
+  try (rewrite <- compare_antisym in Heqc1;
+         rewrite CompOpp_iff in Heqc1;
+         rewrite (compare_trans _ _ _ _ Heqc2 Heqc1) in Heqc0;
+         discriminate);
+  assumption);
+rewrite (compare_trans _ _ _ _ Heqc0 Heqc1);
+try assumption.
+apply (compare_trans _ _ _ _ H H0).
+Qed.
+
+(** Special case of comparable, where equality is usual equality. **)
+Class ComparableUsualEq {A:Type} (C: Comparable A) :=
+  compare_eq : forall x y, compare x y = Eq -> x = y.
+
+(** Boolean equality for a [Comparable]. **)
+Definition compare_eqb {A:Type} {C:Comparable A} (x y:A) :=
+  match compare x y with
+    | Eq => true
+    | _ => false
+  end.
+
+Theorem compare_eqb_iff {A:Type} {C:Comparable A} {U:ComparableUsualEq C} :
+  forall x y, compare_eqb x y = true <-> x = y.
+Proof.
+unfold compare_eqb.
+intuition.
+apply compare_eq.
+destruct (compare x y); intuition; discriminate.
+destruct H.
+rewrite compare_refl; intuition.
+Qed.
+
+(** [Comparable] provides a decidable equality. **)
+Definition compare_eqdec {A:Type} {C:Comparable A} {U:ComparableUsualEq C} (x y:A):
+  {x = y} + {x <> y}.
+Proof.
+destruct (compare x y) as [] eqn:?; [left; apply compare_eq; intuition | ..];
+  right; intro; destruct H; rewrite compare_refl in Heqc; discriminate.
+Defined.
+
+Instance NComparableUsualEq : ComparableUsualEq natComparable := nat_compare_eq.
+
+(** A pair of ComparableUsualEq is ComparableUsualEq **)
+Instance PairComparableUsualEq
+  {A:Type} {CA:Comparable A} (UA:ComparableUsualEq CA)
+  {B:Type} {CB:Comparable B} (UB:ComparableUsualEq CB) :
+    ComparableUsualEq (PairComparable CA CB).
+Proof.
+intros x y; destruct x, y; simpl.
+pose proof (compare_eq a a0); pose proof (compare_eq b b0).
+destruct (compare a a0); try discriminate.
+intuition.
+destruct H2, H0.
+reflexivity.
+Qed.
+
+(** An [Finite] type is a type with the list of all elements. **)
+Class Finite (A:Type) := {
+  all_list : list A;
+  all_list_forall : forall x:A, In x all_list
+}.
+
+(** An alphabet is both [ComparableUsualEq] and [Finite]. **)
+Class Alphabet (A:Type) := {
+  AlphabetComparable :> Comparable A;
+  AlphabetComparableUsualEq :> ComparableUsualEq AlphabetComparable;
+  AlphabetFinite :> Finite A
+}.
+
+(** The [Numbered] class provides a conveniant way to build [Alphabet] instances,
+   with a good computationnal complexity. It is mainly a injection from it to
+   [Int31] **)
+Class Numbered (A:Type) := {
+  inj : A -> int31;
+  surj : int31 -> A;
+  surj_inj_compat : forall x, surj (inj x) = x;
+  inj_bound : int31;
+  inj_bound_spec : forall x, (phi (inj x) < phi inj_bound)%Z
+}.
+
+Program Instance NumberedAlphabet {A:Type} (N:Numbered A) : Alphabet A :=
+  { AlphabetComparable :=
+      {| compare := fun x y => compare31 (inj x) (inj y) |};
+    AlphabetFinite :=
+      {| all_list := fst (iter_int31 inj_bound _ 
+        (fun p => (cons (surj (snd p)) (fst p), incr (snd p))) ([], 0%int31)) |} }.
+Next Obligation. apply Zcompare_antisym. Qed.
+Next Obligation.
+destruct c. unfold compare31 in *.
+rewrite Z.compare_eq_iff in *. congruence.
+eapply Zcompare_Lt_trans; eauto.
+eapply Zcompare_Gt_trans; eauto.
+Qed.
+Next Obligation.
+intros x y H. unfold compare, compare31 in H.
+rewrite Z.compare_eq_iff in *.
+rewrite <- surj_inj_compat, <- phi_inv_phi with (inj y), <- H.
+rewrite phi_inv_phi, surj_inj_compat; reflexivity.
+Qed.
+Next Obligation.
+rewrite iter_int31_iter_nat.
+pose proof (inj_bound_spec x).
+match goal with |- In x (fst ?p) => destruct p as [] eqn:? end.
+replace inj_bound with i in H.
+revert l i Heqp x H.
+apply iter_nat_invariant; intros.
+inversion Heqp; clear Heqp; subst.
+destruct x; specialize (H _ _ (eq_refl _) x0); simpl in *.
+rewrite phi_incr in H0.
+pose proof (phi_bounded i).
+pose proof (phi_bounded (inj x0)).
+destruct (Z_lt_le_dec (Zsucc (phi i)) (2 ^ Z_of_nat size)%Z).
+rewrite Zmod_small in H0 by omega.
+apply Zlt_succ_le, Zle_lt_or_eq in H0.
+destruct H0; eauto.
+left.
+rewrite <- surj_inj_compat, <- phi_inv_phi with (inj x0), H0, phi_inv_phi; reflexivity.
+replace (Zsucc (phi i)) with (2 ^ Z_of_nat size)%Z in H0 by omega.
+rewrite Z_mod_same_full in H0.
+exfalso; omega.
+exfalso; inversion Heqp; subst; 
+  pose proof (phi_bounded (inj x)); change (phi 0) with 0%Z in H; omega.
+clear H.
+rewrite <- phi_inv_phi with i, <- phi_inv_phi with inj_bound; f_equal.
+pose proof (phi_bounded inj_bound); pose proof (phi_bounded i).
+rewrite <- Zabs_eq with (phi i), <- Zabs_eq with (phi inj_bound) by omega.
+clear H H0.
+do 2 rewrite <- inj_Zabs_nat.
+f_equal.
+revert l i Heqp.
+assert (Zabs_nat (phi inj_bound) < Zabs_nat (2^31)).
+apply Zabs_nat_lt, phi_bounded.
+induction (Zabs_nat (phi inj_bound)); intros.
+inversion Heqp; reflexivity.
+inversion Heqp; clear H1 H2 Heqp.
+match goal with |- _ (_ (_ (snd ?p))) = _ => destruct p end.
+pose proof (phi_bounded i0).
+erewrite <- IHn, <- Zabs_nat_Zsucc in H |- *; eauto; try omega.
+rewrite phi_incr, Zmod_small; intuition; try omega.
+apply inj_lt in H.
+pose proof Zle_le_succ.
+do 2 rewrite inj_Zabs_nat, Zabs_eq in H; eauto.
+Qed.
+
+(** Previous class instances for [option A] **)
+Program Instance OptionComparable {A:Type} (C:Comparable A) : Comparable (option A) :=
+  { compare := fun x y =>
+      match x, y return comparison with
+        | None, None => Eq
+        | None, Some _ => Lt
+        | Some _, None => Gt
+        | Some x, Some y => compare x y
+      end }.
+Next Obligation.
+destruct x, y; intuition.
+apply compare_antisym.
+Qed.
+Next Obligation.
+destruct x, y, z; try now intuition;
+try (rewrite <- H in H0; discriminate).
+apply (compare_trans _ _ _ _ H H0).
+Qed.
+
+Instance OptionComparableUsualEq {A:Type} {C:Comparable A} (U:ComparableUsualEq C) :
+  ComparableUsualEq (OptionComparable C).
+Proof.
+intros x y.
+destruct x, y; intuition; try discriminate.
+rewrite (compare_eq a a0); intuition.
+Qed.
+
+Program Instance OptionFinite {A:Type} (E:Finite A) : Finite (option A) :=
+  { all_list := None :: map Some all_list }.
+Next Obligation.
+destruct x; intuition.
+right.
+apply in_map.
+apply all_list_forall.
+Defined.
+
+(** Definitions of [FSet]/[FMap] from [Comparable] **)
+Require Import OrderedType.
+Require Import OrderedTypeAlt.
+Require FSetAVL.
+Require FMapAVL.
+
+Module Type ComparableM.
+  Parameter t : Type.
+  Declare Instance tComparable : Comparable t.
+End ComparableM.
+
+Module OrderedTypeAlt_from_ComparableM (C:ComparableM) <: OrderedTypeAlt.
+  Definition t := C.t.
+  Definition compare : t -> t -> comparison := compare.
+
+  Infix "?=" := compare (at level 70, no associativity).
+
+  Lemma compare_sym x y : (y?=x) = CompOpp (x?=y).
+  Proof. exact (Logic.eq_sym (compare_antisym x y)). Qed.
+  Lemma compare_trans c x y z :
+    (x?=y) = c -> (y?=z) = c -> (x?=z) = c.
+  Proof.
+  apply compare_trans.
+  Qed.
+End OrderedTypeAlt_from_ComparableM.
+
+Module OrderedType_from_ComparableM (C:ComparableM) <: OrderedType.
+  Module Alt := OrderedTypeAlt_from_ComparableM C.
+  Include (OrderedType_from_Alt Alt).
+End OrderedType_from_ComparableM.
diff --git a/cparser/validator/Automaton.v b/cparser/validator/Automaton.v
new file mode 100644
index 0000000..b15f87d
--- /dev/null
+++ b/cparser/validator/Automaton.v
@@ -0,0 +1,167 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Jacques-Henri Jourdan, INRIA Paris-Rocquencourt            *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+Require Grammar.
+Require Import Orders.
+Require Export Alphabet.
+Require Export List.
+Require Export Syntax.
+
+Module Type AutInit.
+  (** The grammar of the automaton. **)
+  Declare Module Gram:Grammar.T.
+  Export Gram.
+
+  (** The set of non initial state is considered as an alphabet. **)
+  Parameter noninitstate : Type.
+  Declare Instance NonInitStateAlph : Alphabet noninitstate.
+
+  Parameter initstate : Type.
+  Declare Instance InitStateAlph : Alphabet initstate.
+
+  (** When we are at this state, we know that this symbol is the top of the
+     stack. **)
+  Parameter last_symb_of_non_init_state: noninitstate -> symbol.
+End AutInit.
+
+Module Types(Import Init:AutInit).
+  (** In many ways, the behaviour of the initial state is different from the
+     behaviour of the other states. So we have chosen to explicitaly separate
+     them: the user has to provide the type of non initial states. **)
+  Inductive state :=
+    | Init: initstate -> state
+    | Ninit: noninitstate -> state.
+
+  Program Instance StateAlph : Alphabet state :=
+    { AlphabetComparable := {| compare := fun x y =>
+        match x, y return comparison with
+          | Init _, Ninit _ => Lt
+          | Init x, Init y => compare x y
+          | Ninit _, Init _ => Gt
+          | Ninit x, Ninit y => compare x y
+        end |};
+      AlphabetFinite := {| all_list := map Init all_list ++ map Ninit all_list |} }.
+  Local Obligation Tactic := intros.
+  Next Obligation.
+  destruct x, y; intuition; apply compare_antisym.
+  Qed.
+  Next Obligation.
+  destruct x, y, z; intuition.
+  apply (compare_trans _ i0); intuition.
+  congruence.
+  congruence.
+  apply (compare_trans _ n0); intuition.
+  Qed.
+  Next Obligation.
+  intros x y.
+  destruct x, y; intuition; try discriminate.
+  rewrite (compare_eq i i0); intuition.
+  rewrite (compare_eq n n0); intuition.
+  Qed.
+  Next Obligation.
+  apply in_or_app; destruct x; intuition;
+    [left|right]; apply in_map; apply  all_list_forall.
+  Qed.
+
+  Coercion Ninit : noninitstate >-> state.
+  Coercion Init : initstate >-> state.
+
+  (** For an LR automaton, there are four kind of actions that can be done at a
+     given state:
+       - Shifting, that is reading a token and putting it into the stack,
+       - Reducing a production, that is popping the right hand side of the
+          production from the stack, and pushing the left hand side,
+       - Failing
+       - Accepting the word (special case of reduction)
+
+     As in the menhir parser generator, we do not want our parser to read after
+     the end of stream. That means that once the parser has read a word in the
+     grammar language, it should stop without peeking the input stream. So, for
+     the automaton to be complete, the grammar must be particular: if a word is
+     in its language, then it is not a prefix of an other word of the language
+     (otherwise, menhir reports an end of stream conflict).
+
+     As a consequence of that, there is two notions of action: the first one is
+     an action performed before having read the stream, the second one is after
+  **)
+
+  Inductive lookahead_action (term:terminal) :=
+  | Shift_act: forall s:noninitstate,
+                 T term = last_symb_of_non_init_state s -> lookahead_action term
+  | Reduce_act: production -> lookahead_action term
+  | Fail_act: lookahead_action term.
+  Implicit Arguments Shift_act [term].
+  Implicit Arguments Reduce_act [term].
+  Implicit Arguments Fail_act [term].
+
+  Inductive action :=
+  | Default_reduce_act: production -> action
+  | Lookahead_act : (forall term:terminal, lookahead_action term) -> action.
+
+  (** Types used for the annotations of the automaton. **)
+
+  (** An item is a part of the annotations given to the validator.
+     It is acually a set of LR(1) items sharing the same core. It is needed 
+     to validate completeness. **)
+  Record item := {
+  (** The pseudo-production of the item. **)
+    prod_item: production;
+
+  (** The position of the dot. **)
+    dot_pos_item: nat;
+
+  (** The lookahead symbol of the item. We are using a list, so we can store
+     together multiple LR(1) items sharing the same core. **)
+    lookaheads_item: list terminal
+  }.
+End Types.
+
+Module Type T.
+  Include AutInit <+ Types.
+  Module Export GramDefs := Grammar.Defs Gram.
+
+  (** For each initial state, the non terminal it recognizes. **)
+  Parameter start_nt: initstate -> nonterminal.
+
+  (** The action table maps a state to either a map terminal -> action. **)
+  Parameter action_table: 
+    state -> action.
+  (** The goto table of an LR(1) automaton. **)
+  Parameter goto_table: state -> forall nt:nonterminal,
+    option { s:noninitstate | NT nt = last_symb_of_non_init_state s }.
+
+  (** Some annotations on the automaton to help the validation. **)
+
+  (** When we are at this state, we know that these symbols are just below
+     the top of the stack. The list is ordered such that the head correspond
+     to the (almost) top of the stack. **)
+  Parameter past_symb_of_non_init_state: noninitstate -> list symbol.
+
+  (** When we are at this state, the (strictly) previous states verify these
+     predicates. **)
+  Parameter past_state_of_non_init_state: noninitstate -> list (state -> bool).
+
+  (** The items of the state. **)
+  Parameter items_of_state: state -> list item.
+
+  (** The nullable predicate for non terminals :
+     true if and only if the symbol produces the empty string **)
+  Parameter nullable_nterm: nonterminal -> bool.
+
+  (** The first predicates for non terminals, symbols or words of symbols. A
+     terminal is in the returned list if, and only if the parameter produces a
+     word that begins with the given terminal **)
+  Parameter first_nterm: nonterminal -> list terminal.
+End T.
diff --git a/cparser/validator/Grammar.v b/cparser/validator/Grammar.v
new file mode 100644
index 0000000..d162892
--- /dev/null
+++ b/cparser/validator/Grammar.v
@@ -0,0 +1,165 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Jacques-Henri Jourdan, INRIA Paris-Rocquencourt            *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+Require Import List.
+Require Import Syntax.
+Require Import Alphabet.
+Require Import Orders.
+
+(** The terminal non-terminal alphabets of the grammar. **)
+Module Type Alphs.
+  Parameters terminal nonterminal : Type.
+  Declare Instance TerminalAlph: Alphabet terminal.
+  Declare Instance NonTerminalAlph: Alphabet nonterminal.
+End Alphs.
+
+(** Definition of the alphabet of symbols, given the alphabet of terminals
+    and the alphabet of non terminals **)
+Module Symbol(Import A:Alphs).
+
+  Inductive symbol :=
+    | T: terminal -> symbol
+    | NT: nonterminal -> symbol.
+
+  Program Instance SymbolAlph : Alphabet symbol :=
+    { AlphabetComparable := {| compare := fun x y =>
+        match x, y return comparison with
+          | T _, NT _ => Gt
+          | NT _, T _ => Lt
+          | T x, T y => compare x y
+          | NT x, NT y => compare x y
+        end |};
+      AlphabetFinite := {| all_list :=
+        map T all_list++map NT all_list |} }.
+  Next Obligation.
+  destruct x; destruct y; intuition; apply compare_antisym.
+  Qed.
+  Next Obligation.
+  destruct x; destruct y; destruct z; intuition; try discriminate.
+  apply (compare_trans _ t0); intuition.
+  apply (compare_trans _ n0); intuition.
+  Qed.
+  Next Obligation.
+  intros x y.
+  destruct x; destruct y; try discriminate; intros.
+  rewrite (compare_eq t t0); intuition.
+  rewrite (compare_eq n n0); intuition.
+  Qed.
+  Next Obligation.
+  rewrite in_app_iff.
+  destruct x; [left | right]; apply in_map; apply all_list_forall.
+  Qed.
+
+End Symbol.
+
+Module Type T.
+  Require Export Tuples.
+
+  Include Alphs <+ Symbol.
+
+  (** [symbol_semantic_type] maps a symbols to the type of its semantic
+     values. **)
+  Parameter symbol_semantic_type: symbol -> Type.
+
+  (** The type of productions identifiers **)
+  Parameter production : Type.
+  Declare Instance ProductionAlph : Alphabet production.
+
+  (** Accessors for productions: left hand side, right hand side,
+     and semantic action. The semantic actions are given in the form
+     of curryfied functions, that take arguments in the reverse order. **)
+  Parameter prod_lhs: production -> nonterminal.
+  Parameter prod_rhs_rev: production -> list symbol.
+  Parameter prod_action:
+    forall p:production,
+      arrows_left
+        (map symbol_semantic_type (rev (prod_rhs_rev p)))
+        (symbol_semantic_type (NT (prod_lhs p))).
+
+End T.
+
+Module Defs(Import G:T).
+
+  (** A token is a terminal and a semantic value for this terminal. **)
+  Definition token := {t:terminal & symbol_semantic_type (T t)}.
+
+  (** A grammar creates a relation between word of tokens and semantic values.
+     This relation is parametrized by the head symbol. It defines the 
+     "semantics" of the grammar. This relation is defined by a notion of 
+     parse tree. **)
+  Inductive parse_tree:
+    forall (head_symbol:symbol) (word:list token)
+      (semantic_value:symbol_semantic_type head_symbol), Type :=
+
+  (** A single token has its semantic value as semantic value, for the
+     corresponding terminal as head symbol. **)
+  | Terminal_pt:
+    forall (t:terminal) (sem:symbol_semantic_type (T t)),
+      parse_tree (T t)
+      [existT (fun t => symbol_semantic_type (T t)) t sem] sem
+
+  (** Given a production, if a word has a list of semantic values for the 
+     right hand side as head symbols, then this word has the semantic value 
+     given by the semantic action of the production for the left hand side 
+     as head symbol.**)
+  | Non_terminal_pt:
+    forall {p:production} {word:list token}
+      {semantic_values:tuple (map symbol_semantic_type (rev (prod_rhs_rev p)))},
+      parse_tree_list (rev (prod_rhs_rev p)) word semantic_values ->
+      parse_tree (NT (prod_lhs p)) word (uncurry (prod_action p) semantic_values)
+
+  (** Basically the same relation as before, but for list of head symbols (ie.
+     We are building a forest of syntax trees. It is mutually recursive with the
+     previous relation **)
+  with parse_tree_list:
+    forall (head_symbols:list symbol) (word:list token)
+      (semantic_values:tuple (map symbol_semantic_type head_symbols)),
+      Type :=
+
+  (** The empty word has [()] as semantic for [[]] as head symbols list **)
+  | Nil_ptl: parse_tree_list [] [] ()
+
+  (** The cons of the semantic value for one head symbol and for a list of head
+     symbols **)
+  | Cons_ptl:
+  (** The semantic for the head **)
+    forall {head_symbolt:symbol} {wordt:list token}
+      {semantic_valuet:symbol_semantic_type head_symbolt},
+      parse_tree head_symbolt wordt semantic_valuet ->
+
+  (** and the semantic for the tail **)
+    forall {head_symbolsq:list symbol} {wordq:list token}
+      {semantic_valuesq:tuple (map symbol_semantic_type head_symbolsq)},
+      parse_tree_list head_symbolsq wordq semantic_valuesq ->
+
+  (** give the semantic of the cons **)
+      parse_tree_list
+        (head_symbolt::head_symbolsq)
+        (wordt++wordq)
+        (semantic_valuet, semantic_valuesq).
+
+
+  Fixpoint pt_size {head_symbol word sem} (tree:parse_tree head_symbol word sem) :=
+    match tree with 
+      | Terminal_pt _ _ => 1
+      | Non_terminal_pt _ _ _ l => S (ptl_size l)
+    end
+  with ptl_size {head_symbols word sems} (tree:parse_tree_list head_symbols word sems) :=
+    match tree with
+      | Nil_ptl => 0
+      | Cons_ptl _ _ _ t _ _ _ q =>
+         pt_size t + ptl_size q
+    end.
+End Defs.
diff --git a/cparser/validator/Interpreter.v b/cparser/validator/Interpreter.v
new file mode 100644
index 0000000..16be385
--- /dev/null
+++ b/cparser/validator/Interpreter.v
@@ -0,0 +1,220 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Jacques-Henri Jourdan, INRIA Paris-Rocquencourt            *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+Require Import Streams.
+Require Import List.
+Require Import Syntax.
+Require Automaton.
+Require Import Alphabet.
+
+Module Make(Import A:Automaton.T).
+
+(** The error monad **)
+Inductive result (A:Type) :=
+  | Err: result A
+  | OK: A -> result A.
+
+Implicit Arguments Err [A].
+Implicit Arguments OK [A].
+
+Definition bind {A B: Type} (f: result A) (g: A -> result B): result B :=
+  match f with
+    | OK x => g x
+    | Err => Err
+  end.
+
+Definition bind2 {A B C: Type} (f: result (A * B)) (g: A -> B -> result C):
+  result C :=
+  match f with
+    | OK (x, y) => g x y
+    | Err => Err
+  end.
+
+Notation "'do' X <- A ; B" := (bind A (fun X => B))
+  (at level 200, X ident, A at level 100, B at level 200).
+
+Notation "'do' ( X , Y ) <- A ; B" := (bind2 A (fun X Y => B))
+  (at level 200, X ident, Y ident, A at level 100, B at level 200).
+
+(** Some operations on streams **)
+
+(** Concatenation of a list and a stream **)
+Fixpoint app_str {A:Type} (l:list A) (s:Stream A) :=
+  match l with
+    | nil => s
+    | cons t q => Cons t (app_str q s)
+  end.
+
+Infix "++" := app_str (right associativity, at level 60).
+
+Lemma app_str_app_assoc {A:Type} (l1 l2:list A) (s:Stream A) :
+  l1 ++ (l2 ++ s) = (l1 ++ l2) ++ s.
+Proof.
+induction l1.
+reflexivity.
+simpl.
+rewrite IHl1.
+reflexivity.
+Qed.
+
+(** The type of a non initial state: the type of semantic values associated
+   with the last symbol of this state. *)
+Definition noninitstate_type state :=
+  symbol_semantic_type (last_symb_of_non_init_state state).
+
+(** The stack of the automaton : it can be either nil or contains a non
+    initial state, a semantic value for the symbol associted with this state,
+    and a nested stack. **)
+Definition stack := list (sigT noninitstate_type). (* eg. list {state & state_type state} *)
+
+Section Init.
+
+Variable init : initstate.
+
+(** The top state of a stack **)
+Definition state_of_stack (stack:stack): state :=
+  match stack with
+    | [] => init
+    | existT s _::_ => s
+  end.
+
+(** [pop] pops some symbols from the stack. It returns the popped semantic
+    values using [sem_popped] as an accumulator and discards the popped
+    states.**)
+Fixpoint pop (symbols_to_pop:list symbol) (stack_cur:stack):
+  forall {A:Type} (action:arrows_right A (map symbol_semantic_type symbols_to_pop)),
+    result (stack * A) :=
+  match symbols_to_pop return forall {A:Type} (action:arrows_right A (map _ symbols_to_pop)), _ with
+    | [] => fun A action => OK (stack_cur, action)
+    | t::q => fun A action => 
+      match stack_cur with
+        | existT state_cur sem::stack_rec =>
+          match compare_eqdec (last_symb_of_non_init_state state_cur) t with
+            | left e =>
+              let sem_conv := eq_rect _ symbol_semantic_type sem _ e in
+                pop q stack_rec (action sem_conv)
+            | right _ => Err
+          end
+        | [] => Err
+      end
+  end.
+
+(** [step_result] represents the result of one step of the automaton : it can
+    fail, accept or progress. [Fail_sr] means that the input is incorrect.
+    [Accept_sr] means that this is the last step of the automaton, and it
+    returns the semantic value of the input word. [Progress_sr] means that
+    some progress has been made, but new steps are needed in order to accept
+    a word.
+
+    For [Accept_sr] and [Progress_sr], the result contains the new input buffer.
+
+    [Fail_sr] means that the input word is rejected by the automaton. It is
+    different to [Err] (from the error monad), which mean that the automaton is
+    bogus and has perfomed a forbidden action. **)
+Inductive step_result :=
+  | Fail_sr: step_result
+  | Accept_sr: symbol_semantic_type (NT (start_nt init)) -> Stream token -> step_result
+  | Progress_sr: stack -> Stream token -> step_result.
+
+Program Definition prod_action':
+  forall p,
+    arrows_right (symbol_semantic_type (NT (prod_lhs p)))
+      (map symbol_semantic_type (prod_rhs_rev p)):=
+      fun p =>
+        eq_rect _ (fun x => x) (prod_action p) _ _.
+Next Obligation.
+unfold arrows_left, arrows_right; simpl.
+rewrite <- fold_left_rev_right, <- map_rev, rev_involutive.
+reflexivity.
+Qed.
+
+(** [reduce_step] does a reduce action :
+   - pops some elements from the stack
+   - execute the action of the production
+   - follows the goto for the produced non terminal symbol **)
+Definition reduce_step stack_cur production buffer: result step_result :=
+  do (stack_new, sem) <-
+    pop (prod_rhs_rev production) stack_cur (prod_action' production);
+  match goto_table (state_of_stack stack_new) (prod_lhs production) return _ with
+    | Some (exist state_new e) =>
+      let sem := eq_rect _ _ sem _ e in
+      OK (Progress_sr (existT noninitstate_type state_new sem::stack_new) buffer)
+    | None =>
+      match stack_new return _ with
+        | [] =>
+          match compare_eqdec (prod_lhs production) (start_nt init) return _ with
+            | left e =>
+              let sem := eq_rect _ (fun nt => _ (_ nt)) sem _ e in
+              OK (Accept_sr sem buffer)
+            | right _ => Err
+          end
+        | _::_ => Err
+      end
+  end.
+
+(** One step of parsing. **)
+Definition step stack_cur buffer: result step_result :=
+  match action_table (state_of_stack stack_cur) with
+    | Default_reduce_act production =>
+      reduce_step stack_cur production buffer
+    | Lookahead_act awt =>
+      match Streams.hd buffer with
+        | existT term sem =>
+          match awt term with
+            | Shift_act state_new e =>
+              let sem_conv := eq_rect _ symbol_semantic_type sem _ e in
+              OK (Progress_sr (existT noninitstate_type state_new sem_conv::stack_cur)
+                              (Streams.tl buffer))
+            | Reduce_act production =>
+              reduce_step stack_cur production buffer
+            | Fail_action =>
+              OK Fail_sr
+          end
+      end
+  end.
+
+(** The parsing use a [nat] parameter [n_steps], so that we do not have to prove
+    terminaison, which is difficult. So the result of a parsing is either
+    a failure (the automaton has rejected the input word), either a timeout
+    (the automaton has spent all the given [n_steps]), either a parsed semantic
+    value with a rest of the input buffer.
+**)
+Inductive parse_result :=
+  | Fail_pr: parse_result
+  | Timeout_pr: parse_result
+  | Parsed_pr: symbol_semantic_type (NT (start_nt init)) -> Stream token -> parse_result.
+
+Fixpoint parse_fix stack_cur buffer n_steps: result parse_result:=
+  match n_steps with
+    | O => OK Timeout_pr
+    | S it =>
+      do r <- step stack_cur buffer;
+      match r with
+        | Fail_sr => OK Fail_pr
+        | Accept_sr t buffer_new => OK (Parsed_pr t buffer_new)
+        | Progress_sr s buffer_new => parse_fix s buffer_new it
+      end
+  end.
+
+Definition parse buffer n_steps: result parse_result :=
+  parse_fix [] buffer n_steps.
+
+End Init.
+
+End Make.
+
+Module Type T(A:Automaton.T).
+  Include (Make A).
+End T.
diff --git a/cparser/validator/Interpreter_complete.v b/cparser/validator/Interpreter_complete.v
new file mode 100644
index 0000000..3b922f7
--- /dev/null
+++ b/cparser/validator/Interpreter_complete.v
@@ -0,0 +1,685 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Jacques-Henri Jourdan, INRIA Paris-Rocquencourt            *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+Require Import Streams.
+Require Import Equality.
+Require Import List.
+Require Import Syntax.
+Require Import Alphabet.
+Require Import Arith.
+Require Grammar.
+Require Automaton.
+Require Interpreter.
+Require Validator_complete.
+
+Module Make(Import A:Automaton.T) (Import Inter:Interpreter.T A).
+Module Import Valid := Validator_complete.Make A.
+
+(** * Completeness Proof **)
+
+Section Completeness_Proof.
+
+Hypothesis complete: complete.
+
+Proposition nullable_stable: nullable_stable.
+Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed.
+Proposition first_stable: first_stable.
+Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed.
+Proposition start_future: start_future.
+Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed.
+Proposition terminal_shift: terminal_shift.
+Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed.
+Proposition end_reduce: end_reduce.
+Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed.
+Proposition start_goto: start_goto.
+Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed.
+Proposition non_terminal_goto: non_terminal_goto.
+Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed.
+Proposition non_terminal_closed: non_terminal_closed.
+Proof. pose proof complete; unfold Valid.complete in H; intuition. Qed.
+
+(** If the nullable predicate has been validated, then it is correct. **)
+Lemma nullable_correct:
+  forall head sem word, word = [] ->
+    parse_tree head word sem -> nullable_symb head = true
+with nullable_correct_list:
+  forall heads sems word, word = [] ->
+    parse_tree_list heads word sems -> nullable_word heads = true.
+Proof with eauto.
+intros.
+destruct X.
+congruence.
+apply nullable_stable...
+intros.
+destruct X; simpl...
+apply andb_true_intro.
+apply app_eq_nil in H; destruct H; split...
+Qed.
+
+(** If the first predicate has been validated, then it is correct. **)
+Lemma first_correct:
+  forall head sem word t q, word = t::q ->
+  parse_tree head word sem ->
+  TerminalSet.In (projT1 t) (first_symb_set head)
+with first_correct_list:
+  forall heads sems word t q, word = t::q ->
+  parse_tree_list heads word sems ->
+  TerminalSet.In (projT1 t) (first_word_set heads).
+Proof with eauto.
+intros.
+destruct X.
+inversion H; subst.
+apply TerminalSet.singleton_2, compare_refl...
+apply first_stable...
+intros.
+destruct X.
+congruence.
+simpl.
+case_eq wordt; intros.
+erewrite nullable_correct...
+apply TerminalSet.union_3.
+subst...
+rewrite H0 in *; inversion H; destruct H2.
+destruct (nullable_symb head_symbolt)...
+apply TerminalSet.union_2...
+Qed.
+
+Variable init: initstate.
+Variable full_word: list token.
+Variable buffer_end: Stream token.
+Variable full_sem: symbol_semantic_type (NT (start_nt init)).
+
+Inductive pt_zipper:
+  forall (hole_symb:symbol) (hole_word:list token) 
+         (hole_sem:symbol_semantic_type hole_symb), Type :=
+| Top_ptz:
+  pt_zipper (NT (start_nt init)) (full_word) (full_sem)
+| Cons_ptl_ptz:
+  forall {head_symbolt:symbol}
+    {wordt:list token}
+    {semantic_valuet:symbol_semantic_type head_symbolt},
+
+  forall {head_symbolsq:list symbol}
+    {wordq:list token}
+    {semantic_valuesq:tuple (map symbol_semantic_type head_symbolsq)},
+    parse_tree_list head_symbolsq wordq semantic_valuesq ->
+      
+    ptl_zipper (head_symbolt::head_symbolsq) (wordt++wordq)
+      (semantic_valuet,semantic_valuesq) ->
+
+    pt_zipper head_symbolt wordt semantic_valuet
+with ptl_zipper:
+  forall (hole_symbs:list symbol) (hole_word:list token)
+         (hole_sems:tuple (map symbol_semantic_type hole_symbs)), Type :=
+| Non_terminal_pt_ptlz:
+  forall {p:production} {word:list token}
+    {semantic_values:tuple (map symbol_semantic_type (rev (prod_rhs_rev p)))},
+    pt_zipper (NT (prod_lhs p)) word (uncurry (prod_action p) semantic_values) ->
+    ptl_zipper (rev (prod_rhs_rev p)) word semantic_values
+
+| Cons_ptl_ptlz:
+  forall {head_symbolt:symbol}
+    {wordt:list token}
+    {semantic_valuet:symbol_semantic_type head_symbolt},
+    parse_tree head_symbolt wordt semantic_valuet ->
+    
+  forall {head_symbolsq:list symbol}
+    {wordq:list token}
+    {semantic_valuesq:tuple (map symbol_semantic_type head_symbolsq)},
+      
+  ptl_zipper (head_symbolt::head_symbolsq) (wordt++wordq)
+    (semantic_valuet,semantic_valuesq) ->
+
+  ptl_zipper head_symbolsq wordq semantic_valuesq.
+
+Fixpoint ptlz_cost {hole_symbs hole_word hole_sems}
+  (ptlz:ptl_zipper hole_symbs hole_word hole_sems) :=
+  match ptlz with
+    | Non_terminal_pt_ptlz _ _ _ ptz =>
+      ptz_cost ptz
+    | Cons_ptl_ptlz _ _ _ pt _ _ _ ptlz' =>
+      ptlz_cost ptlz'
+  end
+with ptz_cost {hole_symb hole_word hole_sem}
+  (ptz:pt_zipper hole_symb hole_word hole_sem) :=
+  match ptz with
+    | Top_ptz => 0
+    | Cons_ptl_ptz _ _ _ _ _ _ ptl ptlz' =>
+      1 + ptl_size ptl + ptlz_cost ptlz'
+  end.
+
+Inductive pt_dot: Type :=
+| Reduce_ptd: ptl_zipper [] [] () -> pt_dot
+| Shift_ptd:
+  forall (term:terminal) (sem: symbol_semantic_type (T term))
+    {symbolsq wordq semsq},
+    parse_tree_list symbolsq wordq semsq ->
+    ptl_zipper (T term::symbolsq) (existT (fun t => symbol_semantic_type (T t)) term sem::wordq) (sem, semsq) ->
+    pt_dot.
+
+Definition ptd_cost (ptd:pt_dot) :=
+  match ptd with
+    | Reduce_ptd ptlz => ptlz_cost ptlz
+    | Shift_ptd _ _ _ _ _ ptl ptlz => 1 + ptl_size ptl + ptlz_cost ptlz
+  end.
+
+Fixpoint ptlz_buffer {hole_symbs hole_word hole_sems}
+  (ptlz:ptl_zipper hole_symbs hole_word hole_sems): Stream token :=
+  match ptlz with
+    | Non_terminal_pt_ptlz _ _ _ ptz =>
+      ptz_buffer ptz
+    | Cons_ptl_ptlz _ _ _ _ _ _ _ ptlz' =>
+      ptlz_buffer ptlz'
+  end
+with ptz_buffer {hole_symb hole_word hole_sem}
+  (ptz:pt_zipper hole_symb hole_word hole_sem): Stream token :=
+  match ptz with
+    | Top_ptz => buffer_end
+    | Cons_ptl_ptz _ _ _ _ wordq _ ptl ptlz' =>
+      wordq++ptlz_buffer ptlz'
+  end.
+
+Definition ptd_buffer (ptd:pt_dot) :=
+  match ptd with
+    | Reduce_ptd ptlz => ptlz_buffer ptlz
+    | Shift_ptd term sem _ wordq _ _ ptlz =>
+      Cons (existT (fun t => symbol_semantic_type (T t)) term sem)
+           (wordq ++ ptlz_buffer ptlz)
+  end.
+
+Fixpoint ptlz_prod {hole_symbs hole_word hole_sems}
+  (ptlz:ptl_zipper hole_symbs hole_word hole_sems): production :=
+  match ptlz with
+    | Non_terminal_pt_ptlz prod _ _ _ => prod
+    | Cons_ptl_ptlz _ _ _ _ _ _ _ ptlz' =>
+      ptlz_prod ptlz'
+  end.
+
+Fixpoint ptlz_past {hole_symbs hole_word hole_sems}
+  (ptlz:ptl_zipper hole_symbs hole_word hole_sems): list symbol :=
+  match ptlz with
+    | Non_terminal_pt_ptlz _ _ _ _ => []
+    | Cons_ptl_ptlz s _ _ _ _ _ _ ptlz' => s::ptlz_past ptlz'
+  end.
+
+Lemma ptlz_past_ptlz_prod:
+  forall hole_symbs hole_word hole_sems
+    (ptlz:ptl_zipper hole_symbs hole_word hole_sems),
+  rev_append hole_symbs (ptlz_past ptlz) = prod_rhs_rev (ptlz_prod ptlz).
+Proof.
+fix 4.
+destruct ptlz; simpl.
+rewrite <- rev_alt, rev_involutive; reflexivity.
+apply (ptlz_past_ptlz_prod _ _ _ ptlz).
+Qed.
+
+Definition ptlz_state_compat {hole_symbs hole_word hole_sems}
+  (ptlz:ptl_zipper hole_symbs hole_word hole_sems)
+  (state:state): Prop :=
+  state_has_future state (ptlz_prod ptlz) hole_symbs
+    (projT1 (Streams.hd (ptlz_buffer ptlz))).
+
+Fixpoint ptlz_stack_compat {hole_symbs hole_word hole_sems}
+  (ptlz:ptl_zipper hole_symbs hole_word hole_sems)
+  (stack:stack): Prop :=
+  ptlz_state_compat ptlz (state_of_stack init stack) /\
+  match ptlz with
+    | Non_terminal_pt_ptlz _ _ _ ptz =>
+      ptz_stack_compat ptz stack
+    | Cons_ptl_ptlz _ _ sem _ _ _ _ ptlz' =>
+      match stack with
+        | [] => False
+        | existT _ sem'::stackq =>
+          ptlz_stack_compat ptlz' stackq /\
+          sem ~= sem'
+      end
+  end
+with ptz_stack_compat {hole_symb hole_word hole_sem}
+  (ptz:pt_zipper hole_symb hole_word hole_sem)
+  (stack:stack): Prop :=
+  match ptz with
+    | Top_ptz => stack = []
+    | Cons_ptl_ptz _ _ _ _ _ _ _ ptlz' =>
+      ptlz_stack_compat ptlz' stack
+  end.
+
+Lemma ptlz_stack_compat_ptlz_state_compat:
+  forall hole_symbs hole_word hole_sems
+    (ptlz:ptl_zipper hole_symbs hole_word hole_sems)
+    (stack:stack),
+    ptlz_stack_compat ptlz stack -> ptlz_state_compat ptlz (state_of_stack init stack).
+Proof.
+destruct ptlz; simpl; intuition.
+Qed.
+
+Definition ptd_stack_compat (ptd:pt_dot) (stack:stack): Prop :=
+  match ptd with
+    | Reduce_ptd ptlz => ptlz_stack_compat ptlz stack
+    | Shift_ptd _ _ _ _ _ _ ptlz => ptlz_stack_compat ptlz stack
+  end.
+
+Fixpoint build_pt_dot {hole_symbs hole_word hole_sems}
+    (ptl:parse_tree_list hole_symbs hole_word hole_sems)
+    (ptlz:ptl_zipper hole_symbs hole_word hole_sems)
+    :pt_dot :=
+  match ptl in parse_tree_list hole_symbs hole_word hole_sems
+    return ptl_zipper hole_symbs hole_word hole_sems -> _ 
+  with
+    | Nil_ptl => fun ptlz =>
+      Reduce_ptd ptlz
+    | Cons_ptl _ _ _ pt _ _ _ ptl' =>
+      match pt in parse_tree hole_symb hole_word hole_sem
+        return ptl_zipper (hole_symb::_) (hole_word++_) (hole_sem,_) -> _
+      with
+        | Terminal_pt term sem => fun ptlz =>
+          Shift_ptd term sem ptl' ptlz
+        | Non_terminal_pt _ _ _ ptl'' => fun ptlz =>
+          build_pt_dot ptl''
+            (Non_terminal_pt_ptlz (Cons_ptl_ptz ptl' ptlz))
+      end
+  end ptlz.
+
+Lemma build_pt_dot_cost:
+  forall hole_symbs hole_word hole_sems 
+    (ptl:parse_tree_list hole_symbs hole_word hole_sems)
+    (ptlz:ptl_zipper hole_symbs hole_word hole_sems),
+    ptd_cost (build_pt_dot ptl ptlz) = ptl_size ptl + ptlz_cost ptlz.
+Proof.
+fix 4.
+destruct ptl; intros.
+reflexivity.
+destruct p.
+reflexivity.
+simpl; rewrite build_pt_dot_cost.
+simpl; rewrite <- plus_n_Sm, plus_assoc; reflexivity.
+Qed.
+
+Lemma build_pt_dot_buffer:
+  forall hole_symbs hole_word hole_sems 
+    (ptl:parse_tree_list hole_symbs hole_word hole_sems)
+    (ptlz:ptl_zipper hole_symbs hole_word hole_sems),
+    ptd_buffer (build_pt_dot ptl ptlz) = hole_word ++ ptlz_buffer ptlz.
+Proof.
+fix 4.
+destruct ptl; intros.
+reflexivity.
+destruct p.
+reflexivity.
+simpl; rewrite build_pt_dot_buffer.
+apply app_str_app_assoc.
+Qed.
+
+Lemma ptd_stack_compat_build_pt_dot: 
+  forall hole_symbs hole_word hole_sems
+    (ptl:parse_tree_list hole_symbs hole_word hole_sems)
+    (ptlz:ptl_zipper hole_symbs hole_word hole_sems)
+    (stack:stack),
+  ptlz_stack_compat ptlz stack ->
+  ptd_stack_compat (build_pt_dot ptl ptlz) stack.
+Proof.
+fix 4.
+destruct ptl; intros.
+eauto.
+destruct p.
+eauto.
+simpl.
+apply ptd_stack_compat_build_pt_dot.
+split.
+apply ptlz_stack_compat_ptlz_state_compat, non_terminal_closed in H.
+apply H; clear H; eauto.
+destruct wordq.
+right; split.
+eauto.
+eapply nullable_correct_list; eauto.
+left.
+eapply first_correct_list; eauto.
+eauto.
+Qed.
+
+Program Fixpoint pop_ptlz {hole_symbs hole_word hole_sems}
+  (ptl:parse_tree_list hole_symbs hole_word hole_sems)
+  (ptlz:ptl_zipper hole_symbs hole_word hole_sems):
+    { word:_ & { sem:_ &
+      (pt_zipper (NT (prod_lhs (ptlz_prod ptlz))) word sem *
+       parse_tree (NT (prod_lhs (ptlz_prod ptlz))) word sem)%type } } :=
+  match ptlz in ptl_zipper hole_symbs hole_word hole_sems 
+    return parse_tree_list hole_symbs hole_word hole_sems -> 
+    { word:_ & { sem:_ &
+      (pt_zipper (NT (prod_lhs (ptlz_prod ptlz))) word sem *
+       parse_tree (NT (prod_lhs (ptlz_prod ptlz))) word sem)%type } }
+  with
+    | Non_terminal_pt_ptlz prod word sem ptz => fun ptl =>
+      let sem := uncurry (prod_action prod) sem in
+      existT _ word (existT _ sem (ptz, Non_terminal_pt ptl))
+    | Cons_ptl_ptlz _ _ _ pt _ _ _ ptlz' => fun ptl =>
+      pop_ptlz (Cons_ptl pt ptl) ptlz'
+  end ptl.
+
+Lemma pop_ptlz_cost:
+  forall hole_symbs hole_word hole_sems 
+    (ptl:parse_tree_list hole_symbs hole_word hole_sems)
+    (ptlz:ptl_zipper hole_symbs hole_word hole_sems),
+  let 'existT word (existT sem (ptz, pt)) := pop_ptlz ptl ptlz in
+  ptlz_cost ptlz = ptz_cost ptz.
+Proof.
+fix 5.
+destruct ptlz.
+reflexivity.
+simpl; apply pop_ptlz_cost.
+Qed.
+
+Lemma pop_ptlz_buffer:
+  forall hole_symbs hole_word hole_sems 
+    (ptl:parse_tree_list hole_symbs hole_word hole_sems)
+    (ptlz:ptl_zipper hole_symbs hole_word hole_sems),
+  let 'existT word (existT sem (ptz, pt)) := pop_ptlz ptl ptlz in
+  ptlz_buffer ptlz = ptz_buffer ptz.
+Proof.
+fix 5.
+destruct ptlz.
+reflexivity.
+simpl; apply pop_ptlz_buffer.
+Qed.
+
+Lemma pop_ptlz_pop_stack_compat_converter:
+  forall A hole_symbs hole_word hole_sems (ptlz:ptl_zipper hole_symbs hole_word hole_sems),
+  arrows_left (map symbol_semantic_type (rev (prod_rhs_rev (ptlz_prod ptlz)))) A =
+  arrows_left (map symbol_semantic_type hole_symbs)
+    (arrows_right A (map symbol_semantic_type (ptlz_past ptlz))).
+Proof.
+intros.
+rewrite <- ptlz_past_ptlz_prod.
+unfold arrows_right, arrows_left.
+rewrite rev_append_rev, map_rev, map_app, map_rev, <- fold_left_rev_right, rev_involutive, fold_right_app.
+rewrite fold_left_rev_right.
+reflexivity.
+Qed.
+
+Lemma pop_ptlz_pop_stack_compat:
+  forall hole_symbs hole_word hole_sems
+    (ptl:parse_tree_list hole_symbs hole_word hole_sems)
+    (ptlz:ptl_zipper hole_symbs hole_word hole_sems)
+    (stack:stack),
+
+    ptlz_stack_compat ptlz stack ->
+    
+    let action' := 
+      eq_rect _ (fun x=>x) (prod_action (ptlz_prod ptlz)) _ 
+      (pop_ptlz_pop_stack_compat_converter _ _ _ _ _)
+    in
+    let 'existT word (existT sem (ptz, pt)) := pop_ptlz ptl ptlz in
+      match pop (ptlz_past ptlz) stack (uncurry action' hole_sems) with
+        | OK (stack', sem') => 
+           ptz_stack_compat ptz stack' /\ sem = sem'
+        | Err => True
+      end.
+Proof.
+Opaque AlphabetComparable AlphabetComparableUsualEq.
+fix 5.
+destruct ptlz. intros; simpl.
+split.
+apply H.
+f_equal.
+apply JMeq_eq, JMeq_sym, JMeq_eqrect with (P:=fun x => x).
+simpl; intros; destruct stack0.
+destruct (proj2 H).
+simpl in H; destruct H.
+destruct s as (state, sem').
+destruct H0.
+specialize (pop_ptlz_pop_stack_compat _ _ _ (Cons_ptl p ptl) ptlz _ H0).
+destruct (pop_ptlz (Cons_ptl p ptl) ptlz) as [word [sem []]].
+destruct (compare_eqdec (last_symb_of_non_init_state state) head_symbolt); intuition.
+eapply JMeq_sym, JMeq_trans, JMeq_sym, JMeq_eq in H1; [|apply JMeq_eqrect with (e:=e)].
+rewrite <- H1.
+simpl in pop_ptlz_pop_stack_compat.
+erewrite proof_irrelevance with (p1:=pop_ptlz_pop_stack_compat_converter _ _ _ _ _).
+apply pop_ptlz_pop_stack_compat.
+Transparent AlphabetComparable AlphabetComparableUsualEq.
+Qed.
+
+Definition next_ptd (ptd:pt_dot): option pt_dot :=
+  match ptd with
+    | Shift_ptd term sem _ _ _ ptl ptlz =>
+      Some (build_pt_dot ptl (Cons_ptl_ptlz (Terminal_pt term sem) ptlz))
+    | Reduce_ptd ptlz =>
+      let 'existT _ (existT _ (ptz, pt)) := pop_ptlz Nil_ptl ptlz in
+      match ptz in pt_zipper sym _ _ return parse_tree sym _ _ -> _ with
+        | Top_ptz => fun pt => None
+        | Cons_ptl_ptz _ _ _ _ _ _ ptl ptlz' =>
+          fun pt => Some (build_pt_dot ptl (Cons_ptl_ptlz pt ptlz'))
+      end pt
+  end.
+
+Lemma next_ptd_cost:
+  forall ptd,
+    match next_ptd ptd with
+      | None => ptd_cost ptd = 0
+      | Some ptd' => ptd_cost ptd = S (ptd_cost ptd')
+    end.
+Proof.
+destruct ptd. unfold next_ptd.
+pose proof (pop_ptlz_cost _ _ _ Nil_ptl p).
+destruct (pop_ptlz Nil_ptl p) as [word[sem[[]]]].
+assumption.
+rewrite build_pt_dot_cost.
+assumption.
+simpl; rewrite build_pt_dot_cost; reflexivity.
+Qed.
+
+Lemma reduce_step_next_ptd:
+  forall (ptlz:ptl_zipper [] [] ()) (stack:stack),
+    ptlz_stack_compat ptlz stack ->
+    match reduce_step init stack (ptlz_prod ptlz) (ptlz_buffer ptlz) with
+      | OK Fail_sr =>
+        False
+      | OK (Accept_sr sem buffer) =>
+        sem = full_sem /\ buffer = buffer_end /\ next_ptd (Reduce_ptd ptlz) = None
+      | OK (Progress_sr stack buffer) =>
+        match next_ptd (Reduce_ptd ptlz) with
+          | None => False
+          | Some ptd =>
+            ptd_stack_compat ptd stack /\ buffer = ptd_buffer ptd
+        end
+      | Err =>
+        True
+    end.
+Proof.
+intros.
+unfold reduce_step, next_ptd.
+apply pop_ptlz_pop_stack_compat with (ptl:=Nil_ptl) in H.
+pose proof (pop_ptlz_buffer _ _ _ Nil_ptl ptlz).
+destruct (pop_ptlz Nil_ptl ptlz) as [word [sem [ptz pt]]].
+rewrite H0; clear H0.
+revert H.
+match goal with 
+  |- match ?p1 with Err => _ | OK _ => _ end -> match bind2 ?p2 _ with Err => _ | OK _ => _ end => 
+  replace p1 with p2; [destruct p2 as [|[]];  intros|]
+end.
+assumption.
+simpl.
+destruct H; subst.
+generalize dependent s0.
+generalize (prod_lhs (ptlz_prod ptlz)); clear ptlz stack0.
+dependent destruction ptz; intros.
+simpl in H; subst; simpl.
+pose proof start_goto; unfold Valid.start_goto in H; rewrite H.
+destruct (compare_eqdec (start_nt init) (start_nt init)); intuition.
+apply JMeq_eq, JMeq_eqrect with (P:=fun nt => symbol_semantic_type (NT nt)).
+pose proof (ptlz_stack_compat_ptlz_state_compat _ _ _ _ _ H).
+apply non_terminal_goto in H0.
+destruct (goto_table (state_of_stack init s) n) as [[]|]; intuition.
+apply ptd_stack_compat_build_pt_dot; simpl; intuition.
+symmetry; apply JMeq_eqrect with (P:=symbol_semantic_type).
+symmetry; apply build_pt_dot_buffer.
+destruct s; intuition.
+simpl in H; apply ptlz_stack_compat_ptlz_state_compat in H.
+destruct (H0 _ _ _ H eq_refl).
+generalize (pop_ptlz_pop_stack_compat_converter (symbol_semantic_type (NT (prod_lhs (ptlz_prod ptlz)))) _ _ _ ptlz).
+pose proof (ptlz_past_ptlz_prod _ _ _ ptlz); simpl in H.
+rewrite H; clear H.
+intro; f_equal; simpl.
+apply JMeq_eq.
+etransitivity.
+apply JMeq_eqrect with (P:=fun x => x).
+symmetry.
+apply JMeq_eqrect with (P:=fun x => x).
+Qed.
+
+Lemma step_next_ptd:
+  forall (ptd:pt_dot) (stack:stack),
+    ptd_stack_compat ptd stack ->
+    match step init stack (ptd_buffer ptd) with
+      | OK Fail_sr =>
+        False
+      | OK (Accept_sr sem buffer) =>
+        sem = full_sem /\ buffer = buffer_end /\ next_ptd ptd = None
+      | OK (Progress_sr stack buffer) =>
+        match next_ptd ptd with
+          | None => False
+          | Some ptd =>
+            ptd_stack_compat ptd stack /\ buffer = ptd_buffer ptd
+        end
+      | Err =>
+        True
+    end.
+Proof.
+intros.
+destruct ptd.
+pose proof (ptlz_stack_compat_ptlz_state_compat _ _ _ _ _ H).
+apply end_reduce in H0.
+unfold step.
+destruct (action_table (state_of_stack init stack0)).
+rewrite H0 by reflexivity.
+apply reduce_step_next_ptd; assumption.
+simpl; destruct (Streams.hd (ptlz_buffer p)); simpl in H0.
+destruct (l x); intuition; rewrite H1.
+apply reduce_step_next_ptd; assumption.
+pose proof (ptlz_stack_compat_ptlz_state_compat _ _ _ _ _ H).
+apply terminal_shift in H0.
+unfold step.
+destruct (action_table (state_of_stack init stack0)); intuition.
+simpl; destruct (Streams.hd (ptlz_buffer p0)) as [] eqn:?.
+destruct (l term); intuition.
+apply ptd_stack_compat_build_pt_dot; simpl; intuition.
+unfold ptlz_state_compat; simpl; destruct Heqt; assumption.
+symmetry; apply JMeq_eqrect with (P:=symbol_semantic_type).
+rewrite build_pt_dot_buffer; reflexivity.
+Qed.
+
+Lemma parse_fix_complete:
+  forall (ptd:pt_dot) (stack:stack) (n_steps:nat),
+    ptd_stack_compat ptd stack ->
+    match parse_fix init stack (ptd_buffer ptd) n_steps with
+      | OK (Parsed_pr sem_res buffer_end_res) =>
+        sem_res = full_sem /\ buffer_end_res = buffer_end /\
+         S (ptd_cost ptd) <= n_steps
+      | OK Fail_pr => False
+      | OK Timeout_pr => n_steps < S (ptd_cost ptd)
+      | Err => True
+    end.
+Proof.
+fix 3.
+destruct n_steps; intros; simpl.
+apply lt_0_Sn.
+apply step_next_ptd in H.
+pose proof (next_ptd_cost ptd).
+destruct (step init stack0 (ptd_buffer ptd)) as [|[]]; simpl; intuition.
+rewrite H3 in H0; rewrite H0.
+apply le_n_S, le_0_n.
+destruct (next_ptd ptd); intuition; subst.
+eapply parse_fix_complete with (n_steps:=n_steps) in H1.
+rewrite H0.
+destruct (parse_fix init s (ptd_buffer p) n_steps) as [|[]]; try assumption.
+apply lt_n_S; assumption.
+destruct H1 as [H1 []]; split; [|split]; try assumption.
+apply le_n_S; assumption.
+Qed.
+
+Variable full_pt: parse_tree (NT (start_nt init)) full_word full_sem.
+
+Definition init_ptd :=
+  match full_pt in parse_tree head full_word full_sem return 
+    pt_zipper head full_word full_sem -> 
+    match head return Type with | T _ => unit | NT _ => pt_dot end
+  with
+    | Terminal_pt _ _ => fun _ => ()
+    | Non_terminal_pt _ _ _ ptl =>
+      fun top => build_pt_dot ptl (Non_terminal_pt_ptlz top)
+  end Top_ptz.
+
+Lemma init_ptd_compat:
+  ptd_stack_compat init_ptd [].
+Proof.
+unfold init_ptd.
+assert (ptz_stack_compat Top_ptz []) by reflexivity.
+pose proof (start_future init); revert H0.
+generalize dependent Top_ptz.
+generalize dependent full_word.
+generalize full_sem.
+generalize (start_nt init).
+dependent destruction full_pt0.
+intros.
+apply ptd_stack_compat_build_pt_dot; simpl; intuition.
+apply H0; reflexivity.
+Qed.
+
+Lemma init_ptd_cost:
+  S (ptd_cost init_ptd) = pt_size full_pt.
+Proof.
+unfold init_ptd.
+assert (ptz_cost Top_ptz = 0) by reflexivity.
+generalize dependent Top_ptz.
+generalize dependent full_word.
+generalize full_sem.
+generalize (start_nt init).
+dependent destruction full_pt0.
+intros.
+rewrite build_pt_dot_cost; simpl.
+rewrite H, plus_0_r; reflexivity.
+Qed.
+
+Lemma init_ptd_buffer:
+  ptd_buffer init_ptd = full_word ++ buffer_end.
+Proof.
+unfold init_ptd.
+assert (ptz_buffer Top_ptz = buffer_end) by reflexivity.
+generalize dependent Top_ptz.
+generalize dependent full_word.
+generalize full_sem.
+generalize (start_nt init).
+dependent destruction full_pt0.
+intros.
+rewrite build_pt_dot_buffer; simpl.
+rewrite H; reflexivity.
+Qed.
+
+Theorem parse_complete n_steps:
+  match parse init (full_word ++ buffer_end) n_steps with
+    | OK (Parsed_pr sem_res buffer_end_res) =>
+      sem_res = full_sem /\ buffer_end_res = buffer_end /\ 
+       pt_size full_pt <= n_steps
+    | OK Fail_pr => False
+    | OK Timeout_pr => n_steps < pt_size full_pt
+    | Err => True
+  end.
+Proof.
+pose proof (parse_fix_complete init_ptd [] n_steps init_ptd_compat).
+rewrite init_ptd_buffer, init_ptd_cost in H.
+apply H.
+Qed.
+
+End Completeness_Proof.
+
+End Make.
diff --git a/cparser/validator/Interpreter_correct.v b/cparser/validator/Interpreter_correct.v
new file mode 100644
index 0000000..095b26c
--- /dev/null
+++ b/cparser/validator/Interpreter_correct.v
@@ -0,0 +1,228 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Jacques-Henri Jourdan, INRIA Paris-Rocquencourt            *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+Require Import Streams.
+Require Import List.
+Require Import Syntax.
+Require Import Equality.
+Require Import Alphabet.
+Require Grammar.
+Require Automaton.
+Require Interpreter.
+
+Module Make(Import A:Automaton.T) (Import Inter:Interpreter.T A).
+
+(** * Correctness of the interpreter **)
+
+(** We prove that, in any case, if the interpreter accepts returning a
+    semantic value, then this is a semantic value of the input **)
+
+Section Init.
+
+Variable init:initstate.
+
+(** [word_has_stack_semantics] relates a word with a state, stating that the
+    word is a concatenation of words that have the semantic values stored in
+    the stack. **)
+Inductive word_has_stack_semantics:
+  forall (word:list token) (stack:stack), Prop :=
+  | Nil_stack_whss: word_has_stack_semantics [] []
+  | Cons_stack_whss:
+    forall (wordq:list token) (stackq:stack),
+      word_has_stack_semantics wordq stackq ->
+
+    forall (wordt:list token) (s:noninitstate)
+           (semantic_valuet:_),
+      inhabited (parse_tree (last_symb_of_non_init_state s) wordt semantic_valuet) ->
+
+    word_has_stack_semantics
+       (wordq++wordt) (existT noninitstate_type s semantic_valuet::stackq).
+
+Lemma pop_invariant_converter:
+  forall A symbols_to_pop symbols_popped,
+  arrows_left (map symbol_semantic_type (rev_append symbols_to_pop symbols_popped)) A =
+  arrows_left (map symbol_semantic_type symbols_popped)
+    (arrows_right A (map symbol_semantic_type symbols_to_pop)).
+Proof.
+intros.
+unfold arrows_right, arrows_left.
+rewrite rev_append_rev, map_app, map_rev, fold_left_app.
+f_equal.
+rewrite <- fold_left_rev_right, rev_involutive.
+reflexivity.
+Qed.
+
+(** [pop] preserves the invariant **)
+Lemma pop_invariant:
+  forall (symbols_to_pop symbols_popped:list symbol)
+         (stack_cur:stack)
+         (A:Type) 
+         (action:arrows_left (map symbol_semantic_type (rev_append symbols_to_pop symbols_popped)) A),
+  forall word_stack word_popped,
+  forall sem_popped,
+    word_has_stack_semantics word_stack stack_cur ->
+    inhabited (parse_tree_list symbols_popped word_popped sem_popped) ->
+    let action' := eq_rect _ (fun x=>x) action _ (pop_invariant_converter _ _ _) in
+    match pop symbols_to_pop stack_cur (uncurry action' sem_popped) with
+      | OK (stack_new, sem) =>
+          exists word1res word2res sem_full,
+            (word_stack = word1res ++ word2res)%list /\
+            word_has_stack_semantics word1res stack_new /\
+            sem = uncurry action sem_full /\
+            inhabited (
+              parse_tree_list (rev_append symbols_to_pop symbols_popped) (word2res++word_popped) sem_full)
+      | Err => True
+    end.
+Proof.
+induction symbols_to_pop; intros; unfold pop; fold pop.
+exists word_stack ([]:list token) sem_popped; intuition.
+f_equal.
+apply JMeq_eq, JMeq_eqrect with (P:=(fun x => x)).
+destruct stack_cur as [|[]]; eauto.
+destruct (compare_eqdec (last_symb_of_non_init_state x) a); eauto.
+destruct e; simpl.
+dependent destruction H.
+destruct H0, H1. apply (Cons_ptl X), inhabits in X0.
+specialize (IHsymbols_to_pop _ _ _ action0 _ _ _ H X0).
+match goal with 
+  IHsymbols_to_pop:match ?p1 with Err => _ | OK _ => _ end |- match ?p2 with Err => _ | OK _ => _ end =>
+    replace p2 with p1; [destruct p1 as [|[]]|]; intuition
+end.
+destruct IHsymbols_to_pop as [word1res [word2res [sem_full []]]]; intuition; subst.
+exists word1res. 
+eexists.
+exists sem_full.
+intuition.
+rewrite <- app_assoc; assumption.
+simpl; f_equal; f_equal.
+apply JMeq_eq.
+etransitivity.
+apply JMeq_eqrect with (P:=(fun x => x)).
+symmetry.
+apply JMeq_eqrect with (P:=(fun x => x)).
+Qed.
+
+(** [reduce_step] preserves the invariant **)
+Lemma reduce_step_invariant (stack:stack) (prod:production):
+  forall word buffer, word_has_stack_semantics word stack ->
+  match reduce_step init stack prod buffer with
+    | OK (Accept_sr sem buffer_new) =>
+      buffer = buffer_new /\
+      inhabited (parse_tree (NT (start_nt init)) word sem)
+    | OK (Progress_sr stack_new buffer_new) =>
+      buffer = buffer_new /\
+      word_has_stack_semantics word stack_new
+    | Err | OK Fail_sr => True
+  end.
+Proof with eauto.
+intros.
+unfold reduce_step.
+pose proof (pop_invariant (prod_rhs_rev prod) [] stack (symbol_semantic_type (NT (prod_lhs prod)))).
+revert H0.
+generalize (pop_invariant_converter (symbol_semantic_type (NT (prod_lhs prod))) (prod_rhs_rev prod) []).
+rewrite <- rev_alt.
+intros.
+specialize (H0 (prod_action prod) _ [] () H (inhabits Nil_ptl)).
+match goal with H0:let action' := ?a in _ |- _ => replace a with (prod_action' prod) in H0 end.
+simpl in H0.
+destruct (pop (prod_rhs_rev prod) stack (prod_action' prod)) as [|[]]; intuition.
+destruct H0 as [word1res [word2res [sem_full]]]; intuition.
+destruct H4; apply Non_terminal_pt, inhabits in X.
+match goal with X:inhabited (parse_tree _ _ ?u) |- _ => replace u with s0 in X end.
+clear sem_full H2.
+simpl; destruct (goto_table (state_of_stack init s) (prod_lhs prod)) as [[]|]; intuition; subst.
+rewrite app_nil_r in X; revert s0 X; rewrite e0; intro; simpl.
+constructor...
+destruct s; intuition.
+destruct (compare_eqdec (prod_lhs prod) (start_nt init)); intuition.
+rewrite app_nil_r in X.
+rewrite <- e0.
+inversion H0.
+destruct X; constructor...
+apply JMeq_eq.
+etransitivity.
+apply JMeq_eqrect with (P:=(fun x => x)).
+symmetry.
+apply JMeq_eqrect with (P:=(fun x => x)).
+Qed.
+
+(** [step] preserves the invariant **)
+Lemma step_invariant (stack:stack) (buffer:Stream token):
+  forall buffer_tmp,
+  (exists word_old,
+    buffer = word_old ++ buffer_tmp /\
+    word_has_stack_semantics word_old stack) ->
+  match step init stack buffer_tmp with
+    | OK (Accept_sr sem buffer_new) =>
+      exists word_new,
+        buffer = word_new ++ buffer_new /\
+        inhabited (parse_tree (NT (start_nt init)) word_new sem)
+    | OK (Progress_sr stack_new buffer_new) =>
+      exists word_new,
+        buffer = word_new ++ buffer_new /\
+        word_has_stack_semantics word_new stack_new
+    | Err | OK Fail_sr => True
+  end.
+Proof with eauto.
+intros.
+destruct H, H.
+unfold step.
+destruct (action_table (state_of_stack init stack)).
+pose proof (reduce_step_invariant stack p x buffer_tmp).
+destruct (reduce_step init stack p buffer_tmp) as [|[]]; intuition; subst...
+destruct buffer_tmp.
+unfold Streams.hd.
+destruct t.
+destruct (l x0); intuition.
+exists (x ++ [existT (fun t => symbol_semantic_type (T t)) x0 s])%list.
+split.
+now rewrite <- app_str_app_assoc; intuition.
+apply Cons_stack_whss; intuition.
+destruct e; simpl.
+now exact (inhabits (Terminal_pt _ _)).
+match goal with |- (match reduce_step init stack p ?buff with Err => _ | OK _ => _ end) =>
+  pose proof (reduce_step_invariant stack p x buff);
+  destruct (reduce_step init stack p buff) as [|[]]; intuition; subst
+end...
+Qed.
+
+(** The interpreter is correct : if it returns a semantic value, then the input
+    word has this semantic value.
+**)
+Theorem parse_correct buffer n_steps:
+  match parse init buffer n_steps with
+    | OK (Parsed_pr sem buffer_new) =>
+      exists word_new,
+        buffer = word_new ++ buffer_new /\
+        inhabited (parse_tree (NT (start_nt init)) word_new sem)
+    | _ => True
+  end.
+Proof.
+unfold parse.
+assert (exists w, buffer = w ++ buffer /\ word_has_stack_semantics w []).
+exists ([]:list token); intuition.
+now apply Nil_stack_whss.
+revert H.
+generalize ([]:stack), buffer at 2 3.
+induction n_steps; simpl; intuition.
+pose proof (step_invariant _ _ _ H).
+destruct (step init s buffer0); simpl; intuition.
+destruct s0; intuition.
+apply IHn_steps; intuition.
+Qed.
+
+End Init.
+
+End Make.
diff --git a/cparser/validator/Interpreter_safe.v b/cparser/validator/Interpreter_safe.v
new file mode 100644
index 0000000..f094ddc
--- /dev/null
+++ b/cparser/validator/Interpreter_safe.v
@@ -0,0 +1,275 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Jacques-Henri Jourdan, INRIA Paris-Rocquencourt            *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+Require Import Streams.
+Require Import Equality.
+Require Import List.
+Require Import Syntax.
+Require Import Alphabet.
+Require Grammar.
+Require Automaton.
+Require Validator_safe.
+Require Interpreter.
+
+Module Make(Import A:Automaton.T) (Import Inter:Interpreter.T A).
+Module Import Valid := Validator_safe.Make A.
+
+(** * A correct automaton does not crash **)
+
+Section Safety_proof.
+
+Hypothesis safe: safe.
+
+Proposition shift_head_symbs: shift_head_symbs.
+Proof. pose proof safe; unfold Valid.safe in H; intuition. Qed.
+Proposition goto_head_symbs: goto_head_symbs.
+Proof. pose proof safe; unfold Valid.safe in H; intuition. Qed.
+Proposition shift_past_state: shift_past_state.
+Proof. pose proof safe; unfold Valid.safe in H; intuition. Qed.
+Proposition goto_past_state: goto_past_state.
+Proof. pose proof safe; unfold Valid.safe in H; intuition. Qed.
+Proposition reduce_ok: reduce_ok.
+Proof. pose proof safe; unfold Valid.safe in H; intuition. Qed.
+
+(** We prove that a correct automaton won't crash : the interpreter will
+    not return [Err] **)
+
+Variable init : initstate.
+
+(** The stack of states of an automaton stack **)
+Definition state_stack_of_stack (stack:stack) :=
+  (List.map
+    (fun cell:sigT noninitstate_type => singleton_state_pred (projT1 cell))
+    stack ++ [singleton_state_pred init])%list.
+
+(** The stack of symbols of an automaton stack **)
+Definition symb_stack_of_stack (stack:stack) :=
+  List.map
+    (fun cell:sigT noninitstate_type => last_symb_of_non_init_state (projT1 cell))
+    stack.
+
+(** The stack invariant : it basically states that the assumptions on the
+    states are true. **)
+Inductive stack_invariant: stack -> Prop :=
+  | stack_invariant_constr:
+    forall stack,
+      prefix      (head_symbs_of_state (state_of_stack init stack))
+                  (symb_stack_of_stack stack) ->
+      prefix_pred (head_states_of_state (state_of_stack init stack))
+                  (state_stack_of_stack stack) ->
+      stack_invariant_rec stack ->
+      stack_invariant stack
+with stack_invariant_rec: stack -> Prop :=
+  | stack_invariant_rec_nil:
+      stack_invariant_rec []
+  | stack_invariant_rec_cons:
+    forall state_cur st stack_rec,
+      stack_invariant stack_rec ->
+      stack_invariant_rec (existT _ state_cur st::stack_rec).
+
+(** [pop] conserves the stack invariant and does not crash
+     under the assumption that we can pop at this place.
+     Moreover, after a pop, the top state of the stack is allowed. **)
+Lemma pop_stack_invariant_conserved
+  (symbols_to_pop:list symbol) (stack_cur:stack) A action:
+  stack_invariant stack_cur ->
+  prefix symbols_to_pop (head_symbs_of_state (state_of_stack init stack_cur)) ->
+  match pop symbols_to_pop stack_cur (A:=A) action with
+    | OK (stack_new, _) =>
+      stack_invariant stack_new /\
+      state_valid_after_pop
+        (state_of_stack init stack_new) symbols_to_pop
+        (head_states_of_state (state_of_stack init stack_cur))
+    | Err => False
+  end.
+Proof with eauto.
+  intros.
+  pose proof H.
+  destruct H.
+  revert H H0 H1 H2 H3.
+  generalize (head_symbs_of_state (state_of_stack init stack0)).
+  generalize (head_states_of_state (state_of_stack init stack0)).
+  revert stack0 A action.
+  induction symbols_to_pop; intros.
+  - split...
+    destruct l; constructor.
+    inversion H2; subst.
+    specialize (H7 (state_of_stack init stack0)).
+    destruct (f2 (state_of_stack init stack0)) as [] eqn:? ...
+    destruct stack0 as [|[]]; simpl in *.
+    + inversion H6; subst.
+      unfold singleton_state_pred in Heqb0.
+      now rewrite compare_refl in Heqb0; discriminate.
+    + inversion H6; subst.
+      unfold singleton_state_pred in Heqb0.
+      now rewrite compare_refl in Heqb0; discriminate.
+  - destruct stack0 as [|[]]; unfold pop.
+    + inversion H0; subst.
+      now inversion H.
+    + fold pop.
+      destruct (compare_eqdec (last_symb_of_non_init_state x) a).
+      * inversion H0; subst. clear H0.
+        inversion H; subst. clear H.
+        dependent destruction H3; simpl.
+        assert (prefix_pred (List.tl l) (state_stack_of_stack stack0)).
+        unfold tl; destruct l; [constructor | inversion H2]...
+        pose proof H. destruct H3.
+        specialize (IHsymbols_to_pop stack0 A (action0 n) _ _ H4 H7 H H0 H6).
+        revert IHsymbols_to_pop.
+        fold (noninitstate_type x); generalize (pop symbols_to_pop stack0 (action0 n)).
+        destruct r as [|[]]; intuition...
+        destruct l; constructor...
+      * apply n0.
+        inversion H0; subst.
+        inversion H; subst...
+Qed.
+
+(** [prefix] is associative **)
+Lemma prefix_ass:
+  forall (l1 l2 l3:list symbol), prefix l1 l2 -> prefix l2 l3 -> prefix l1 l3.
+Proof.
+induction l1; intros.
+constructor.
+inversion H; subst.
+inversion H0; subst.
+constructor; eauto.
+Qed.
+
+(** [prefix_pred] is associative **)
+Lemma prefix_pred_ass:
+  forall (l1 l2 l3:list (state->bool)),
+  prefix_pred l1 l2 -> prefix_pred l2 l3 -> prefix_pred l1 l3.
+Proof.
+induction l1; intros.
+constructor.
+inversion H; subst.
+inversion H0; subst.
+constructor; eauto.
+intro.
+specialize (H3 x).
+specialize (H4 x).
+destruct (f0 x); simpl in *; intuition.
+rewrite H4 in H3; intuition.
+Qed.
+
+(** If we have the right to reduce at this state, then the stack invariant
+   is conserved by [reduce_step] and [reduce_step] does not crash. **)
+Lemma reduce_step_stack_invariant_conserved stack prod buff:
+  stack_invariant stack ->
+  valid_for_reduce (state_of_stack init stack) prod ->
+  match reduce_step init stack prod buff with
+    | OK (Fail_sr | Accept_sr _ _) => True
+    | OK (Progress_sr stack_new _) => stack_invariant stack_new
+    | Err => False
+  end.
+Proof with eauto.
+unfold valid_for_reduce.
+intuition.
+unfold reduce_step.
+pose proof (pop_stack_invariant_conserved (prod_rhs_rev prod) stack _ (prod_action' prod)).
+destruct (pop (prod_rhs_rev prod) stack (prod_action' prod)) as [|[]].
+apply H0...
+destruct H0...
+pose proof (goto_head_symbs (state_of_stack init s) (prod_lhs prod)).
+pose proof (goto_past_state (state_of_stack init s) (prod_lhs prod)).
+unfold bind2.
+destruct H0.
+specialize (H2 _ H3)...
+destruct (goto_table (state_of_stack init stack0) (prod_lhs prod)) as [[]|].
+constructor.
+simpl.
+constructor.
+eapply prefix_ass...
+unfold state_stack_of_stack; simpl; constructor.
+intro; destruct (singleton_state_pred x x0); reflexivity.
+eapply prefix_pred_ass...
+constructor...
+constructor...
+destruct stack0 as [|[]]...
+destruct (compare_eqdec (prod_lhs prod) (start_nt init))...
+apply n, H2, eq_refl.
+apply H2, eq_refl.
+Qed.
+
+(** If the automaton is safe, then the stack invariant is conserved by
+    [step] and [step] does not crash. **)
+Lemma step_stack_invariant_conserved (stack:stack) buffer:
+  stack_invariant stack ->
+  match step init stack buffer with
+    | OK (Fail_sr | Accept_sr _ _) => True
+    | OK (Progress_sr stack_new _) => stack_invariant stack_new
+    | Err => False
+  end.
+Proof with eauto.
+intro.
+unfold step.
+pose proof (shift_head_symbs (state_of_stack init stack)).
+pose proof (shift_past_state (state_of_stack init stack)).
+pose proof (reduce_ok (state_of_stack init stack)).
+destruct (action_table (state_of_stack init stack)).
+apply reduce_step_stack_invariant_conserved...
+destruct buffer as [[]]; simpl.
+specialize (H0 x); specialize (H1 x); specialize (H2 x).
+destruct (l x)...
+destruct H.
+constructor.
+unfold state_of_stack.
+constructor.
+eapply prefix_ass...
+unfold state_stack_of_stack; simpl; constructor.
+intro; destruct (singleton_state_pred s0 x0)...
+eapply prefix_pred_ass...
+constructor...
+constructor...
+apply reduce_step_stack_invariant_conserved...
+Qed.
+
+(** If the automaton is safe, then it does not crash **)
+Theorem parse_no_err buffer n_steps:
+  parse init buffer n_steps <> Err.
+Proof with eauto.
+unfold parse.
+assert (stack_invariant []).
+constructor.
+constructor.
+unfold state_stack_of_stack; simpl; constructor.
+intro; destruct (singleton_state_pred init x)...
+constructor.
+constructor.
+revert H.
+generalize buffer ([]:stack).
+induction n_steps; simpl.
+now discriminate.
+intros.
+pose proof (step_stack_invariant_conserved s buffer0 H).
+destruct (step init s buffer0) as [|[]]; simpl...
+discriminate.
+discriminate.
+Qed.
+
+(** A version of [parse] that uses safeness in order to return a
+   [parse_result], and not a [result parse_result] : we have proven that
+   parsing does not return [Err]. **)
+Definition parse_with_safe (buffer:Stream token) (n_steps:nat):
+  parse_result init.
+Proof with eauto.
+pose proof (parse_no_err buffer n_steps).
+destruct (parse init buffer n_steps)...
+congruence.
+Defined.
+
+End Safety_proof.
+
+End Make.
diff --git a/cparser/validator/Main.v b/cparser/validator/Main.v
new file mode 100644
index 0000000..1a17e98
--- /dev/null
+++ b/cparser/validator/Main.v
@@ -0,0 +1,92 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Jacques-Henri Jourdan, INRIA Paris-Rocquencourt            *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+Require Grammar.
+Require Automaton.
+Require Interpreter_safe.
+Require Interpreter_correct.
+Require Interpreter_complete.
+Require Import Syntax.
+
+Module Make(Export Aut:Automaton.T).
+Export Aut.Gram.
+Export Aut.GramDefs.
+
+Module Import Inter := Interpreter.Make Aut.
+Module Safe := Interpreter_safe.Make Aut Inter.
+Module Correct := Interpreter_correct.Make Aut Inter.
+Module Complete := Interpreter_complete.Make Aut Inter.
+
+Definition complete_validator:unit->bool := Complete.Valid.is_complete.
+Definition safe_validator:unit->bool := Safe.Valid.is_safe.
+Definition parse (safe:safe_validator ()=true) init n_steps buffer : parse_result init:=
+  Safe.parse_with_safe (Safe.Valid.is_safe_correct safe) init buffer n_steps.
+
+(** Correction theorem. **)
+Theorem parse_correct
+  (safe:safe_validator ()= true) init n_steps buffer:
+  match parse safe init n_steps buffer with
+    | Parsed_pr sem buffer_new =>
+      exists word,
+        buffer = word ++ buffer_new /\ inhabited (parse_tree (NT (start_nt init)) word sem)
+    | _ => True
+  end.
+Proof.
+unfold parse, Safe.parse_with_safe.
+pose proof (Correct.parse_correct init buffer n_steps).
+generalize (Safe.parse_no_err (Safe.Valid.is_safe_correct safe) init buffer n_steps).
+destruct (Inter.parse init buffer n_steps); intros.
+now destruct (n (eq_refl _)).
+now destruct p; trivial.
+Qed.
+
+(** Completeness theorem. **)
+Theorem parse_complete
+  (safe:safe_validator () = true) init n_steps word buffer_end sem:
+  complete_validator () = true ->
+  forall tree:parse_tree (NT (start_nt init)) word sem,
+  match parse safe init n_steps (word ++ buffer_end) with
+    | Fail_pr => False
+    | Parsed_pr sem_res buffer_end_res =>
+      sem_res = sem /\ buffer_end_res = buffer_end /\ pt_size tree <= n_steps
+    | Timeout_pr => n_steps < pt_size tree
+  end.
+Proof.
+intros.
+unfold parse, Safe.parse_with_safe.
+pose proof (Complete.parse_complete (Complete.Valid.is_complete_correct H) init _ buffer_end _ tree n_steps).
+generalize (Safe.parse_no_err (Safe.Valid.is_safe_correct safe) init (word ++ buffer_end) n_steps).
+destruct (Inter.parse init (word ++ buffer_end) n_steps); intros.
+now destruct (n eq_refl).
+now exact H0.
+Qed.
+
+(** Unambiguity theorem. **)
+Theorem unambiguity:
+  safe_validator () = true -> complete_validator () = true -> inhabited token ->
+  forall init word,
+  forall sem1 (tree1:parse_tree (NT (start_nt init)) word sem1),
+  forall sem2 (tree2:parse_tree (NT (start_nt init)) word sem2),
+  sem1 = sem2.
+Proof.
+intros.
+destruct H1.
+pose proof (parse_complete H init (pt_size tree1) word (Streams.const X) sem1) H0 tree1.
+pose proof (parse_complete H init (pt_size tree1) word (Streams.const X) sem2) H0 tree2.
+destruct (parse H init (pt_size tree1) (word ++ Streams.const X)); intuition.
+rewrite <- H3, H1; reflexivity.
+Qed.
+
+End Make.
diff --git a/cparser/validator/Tuples.v b/cparser/validator/Tuples.v
new file mode 100644
index 0000000..88dc46e
--- /dev/null
+++ b/cparser/validator/Tuples.v
@@ -0,0 +1,46 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Jacques-Henri Jourdan, INRIA Paris-Rocquencourt            *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+Require Import List.
+Require Import Coq.Program.Syntax.
+Require Import Equality.
+
+(** A curryfied function with multiple parameters **)
+Definition arrows_left: list Type -> Type -> Type :=
+  fold_left (fun A B => B -> A).
+
+(** A curryfied function with multiple parameters **)
+Definition arrows_right: Type -> list Type -> Type :=
+  fold_right (fun A B => A -> B).
+
+(** A tuple is a heterogeneous list. For convenience, we use pairs. **)
+Definition tuple (types:list Type) : Type :=
+  fold_right prod unit types.
+
+Fixpoint uncurry {args:list Type} {res:Type}:
+  arrows_left args res -> tuple args -> res :=
+  match args return forall res, arrows_left args res -> tuple args -> res with
+    | [] => fun _ f _ => f
+    | t::q => fun res f p => let (d, t) := p in
+      (@uncurry q _ f t) d
+  end res.
+
+Lemma JMeq_eqrect:
+  forall (U:Type) (a b:U) (P:U -> Type) (x:P a) (e:a=b),
+    eq_rect a P x b e ~= x.
+Proof.
+destruct e.
+reflexivity.
+Qed.
diff --git a/cparser/validator/Validator_complete.v b/cparser/validator/Validator_complete.v
new file mode 100644
index 0000000..9855930
--- /dev/null
+++ b/cparser/validator/Validator_complete.v
@@ -0,0 +1,525 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Jacques-Henri Jourdan, INRIA Paris-Rocquencourt            *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+Require Automaton.
+Require Import Alphabet.
+Require Import List.
+Require Import Syntax.
+
+Module Make(Import A:Automaton.T).
+
+(** We instantiate some sets/map. **)
+Module TerminalComparableM <: ComparableM.
+  Definition t := terminal.
+  Instance tComparable : Comparable t := _.
+End TerminalComparableM.
+Module TerminalOrderedType := OrderedType_from_ComparableM TerminalComparableM.
+Module StateProdPosComparableM <: ComparableM.
+  Definition t := (state*production*nat)%type.
+  Instance tComparable : Comparable t := _.
+End StateProdPosComparableM.
+Module StateProdPosOrderedType :=
+  OrderedType_from_ComparableM StateProdPosComparableM.
+
+Module TerminalSet := FSetAVL.Make TerminalOrderedType.
+Module StateProdPosMap := FMapAVL.Make StateProdPosOrderedType.
+
+(** Nullable predicate for symbols and list of symbols. **)
+Definition nullable_symb (symbol:symbol) :=
+  match symbol with
+    | NT nt => nullable_nterm nt
+    | _ => false
+  end.
+
+Definition nullable_word (word:list symbol) :=
+  forallb nullable_symb word.
+
+(** First predicate for non terminal, symbols and list of symbols, given as FSets. **)
+Definition first_nterm_set (nterm:nonterminal) :=
+  fold_left (fun acc t => TerminalSet.add t acc)
+    (first_nterm nterm) TerminalSet.empty.
+
+Definition first_symb_set (symbol:symbol) :=
+  match symbol with
+    | NT nt => first_nterm_set nt
+    | T t => TerminalSet.singleton t
+  end.
+
+Fixpoint first_word_set (word:list symbol) :=
+  match word with
+    | [] => TerminalSet.empty
+    | t::q =>
+      if nullable_symb t then
+        TerminalSet.union (first_symb_set t) (first_word_set q)
+        else
+          first_symb_set t
+  end.
+
+(** Small helper for finding the part of an item that is after the dot. **)
+Definition future_of_prod prod dot_pos : list symbol :=
+  (fix loop n lst :=
+    match n with
+      | O => lst
+      | S x => match loop x lst with [] => [] | _::q => q end
+    end)
+  dot_pos (rev' (prod_rhs_rev prod)).
+
+(** We build a fast map to store all the items of all the states. **)
+Definition items_map (_:unit): StateProdPosMap.t TerminalSet.t :=
+  fold_left (fun acc state =>
+    fold_left (fun acc item =>
+      let key := (state, prod_item item, dot_pos_item item) in
+        let data := fold_left (fun acc t => TerminalSet.add t acc)
+          (lookaheads_item item) TerminalSet.empty
+        in
+        let old :=
+          match StateProdPosMap.find key acc with
+            | Some x => x | None => TerminalSet.empty
+          end
+        in
+        StateProdPosMap.add key (TerminalSet.union data old) acc
+    ) (items_of_state state) acc
+  ) all_list (StateProdPosMap.empty TerminalSet.t).
+
+(** Accessor. **)
+Definition find_items_map items_map state prod dot_pos : TerminalSet.t :=
+  match StateProdPosMap.find (state, prod, dot_pos) items_map with
+    | None => TerminalSet.empty
+    | Some x => x
+  end.
+
+Definition state_has_future state prod (fut:list symbol) (lookahead:terminal) :=
+  exists dot_pos:nat,
+    fut = future_of_prod prod dot_pos /\
+    TerminalSet.In lookahead (find_items_map (items_map ()) state prod dot_pos).
+
+(** Iterator over items. **)
+Definition forallb_items items_map (P:state -> production -> nat -> TerminalSet.t -> bool): bool:=
+  StateProdPosMap.fold (fun key set acc =>
+    match key with (st, p, pos) => (acc && P st p pos set)%bool end
+  ) items_map true.
+
+Lemma forallb_items_spec :
+  forall p, forallb_items (items_map ()) p = true ->
+  forall st prod fut lookahead, state_has_future st prod fut lookahead ->
+  forall P:state -> production -> list symbol -> terminal -> Prop,
+  (forall st prod pos set lookahead,
+    TerminalSet.In lookahead set -> p st prod pos set = true ->
+      P st prod (future_of_prod prod pos) lookahead) ->
+   P st prod fut lookahead.
+Proof.
+intros.
+unfold forallb_items in H.
+rewrite StateProdPosMap.fold_1 in H.
+destruct H0; destruct H0.
+specialize (H1 st prod x _ _ H2).
+destruct H0.
+apply H1.
+unfold find_items_map in *.
+pose proof (@StateProdPosMap.find_2 _ (items_map ()) (st, prod, x)).
+destruct (StateProdPosMap.find (st, prod, x) (items_map ())); [ |destruct (TerminalSet.empty_1 H2)].
+specialize (H0 _ (eq_refl _)).
+pose proof (StateProdPosMap.elements_1 H0).
+revert H.
+generalize true at 1.
+induction H3.
+destruct H.
+destruct y.
+simpl in H3; destruct H3.
+pose proof (compare_eq (st, prod, x) k H).
+destruct H3.
+simpl.
+generalize (p st prod x t).
+induction l; simpl; intros.
+rewrite Bool.andb_true_iff in H3.
+intuition.
+destruct a; destruct k; destruct p0.
+simpl in H3.
+replace (b0 && b && p s p0 n t0)%bool with (b0 && p s p0 n t0 && b)%bool in H3.
+apply (IHl _ _ H3).
+destruct b, b0, (p s p0 n t0); reflexivity.
+intro.
+apply IHInA.
+Qed.
+
+(** * Validation for completeness **)
+
+(** The nullable predicate is a fixpoint : it is correct. **)
+Definition nullable_stable:=
+  forall p:production,
+    nullable_word (rev (prod_rhs_rev p)) = true ->
+    nullable_nterm (prod_lhs p) = true.
+
+Definition is_nullable_stable (_:unit) :=
+  forallb (fun p:production =>
+    implb (nullable_word (rev' (prod_rhs_rev p))) (nullable_nterm (prod_lhs p)))
+    all_list.
+
+Property is_nullable_stable_correct :
+  is_nullable_stable () = true -> nullable_stable.
+Proof.
+unfold is_nullable_stable, nullable_stable.
+intros.
+rewrite forallb_forall in H.
+specialize (H p (all_list_forall p)).
+unfold rev' in H; rewrite <- rev_alt in H.
+rewrite H0 in H; intuition.
+Qed.
+
+(** The first predicate is a fixpoint : it is correct. **)
+Definition first_stable:=
+  forall (p:production),
+    TerminalSet.Subset (first_word_set (rev (prod_rhs_rev p)))
+                       (first_nterm_set (prod_lhs p)).
+
+Definition is_first_stable (_:unit) :=
+  forallb (fun p:production =>
+    TerminalSet.subset (first_word_set (rev' (prod_rhs_rev p)))
+                       (first_nterm_set (prod_lhs p)))
+    all_list.
+
+Property is_first_stable_correct :
+  is_first_stable () = true -> first_stable.
+Proof.
+unfold is_first_stable, first_stable.
+intros.
+rewrite forallb_forall in H.
+specialize (H p (all_list_forall p)).
+unfold rev' in H; rewrite <- rev_alt in H.
+apply TerminalSet.subset_2; intuition.
+Qed.
+
+(** The initial state has all the S=>.u items, where S is the start non-terminal **)
+Definition start_future :=
+  forall (init:initstate) (t:terminal) (p:production),
+    prod_lhs p = start_nt init ->
+    state_has_future init p (rev (prod_rhs_rev p)) t.
+
+Definition is_start_future items_map :=
+  forallb (fun init =>
+    forallb (fun prod =>
+      if compare_eqb (prod_lhs prod) (start_nt init) then
+        let lookaheads := find_items_map items_map init prod 0 in
+          forallb (fun t => TerminalSet.mem t lookaheads) all_list
+        else
+          true) all_list) all_list.
+
+Property is_start_future_correct :
+  is_start_future (items_map ()) = true -> start_future.
+Proof.
+unfold is_start_future, start_future.
+intros.
+rewrite forallb_forall in H.
+specialize (H init (all_list_forall _)).
+rewrite forallb_forall in H.
+specialize (H p (all_list_forall _)).
+rewrite <- compare_eqb_iff in H0.
+rewrite H0 in H.
+rewrite forallb_forall in H.
+specialize (H t (all_list_forall _)).
+exists 0.
+split.
+apply rev_alt.
+apply TerminalSet.mem_2; eauto.
+Qed.
+
+(** If a state contains an item of the form A->_.av[[b]], where a is a
+    terminal, then reading an a does a [Shift_act], to a state containing
+    an item of the form A->_.v[[b]]. **)
+Definition terminal_shift :=
+  forall (s1:state) prod fut lookahead,
+    state_has_future s1 prod fut lookahead ->
+    match fut with
+      | T t::q =>
+        match action_table s1 with
+          | Lookahead_act awp =>
+            match awp t with
+              | Shift_act s2 _ =>
+                state_has_future s2 prod q lookahead
+              | _ => False
+            end
+          | _ => False
+        end
+      | _ => True
+    end.
+
+Definition is_terminal_shift items_map :=
+  forallb_items items_map (fun s1 prod pos lset =>
+    match future_of_prod prod pos with
+      | T t::_ =>
+        match action_table s1 with
+          | Lookahead_act awp =>
+            match awp t with
+              | Shift_act s2 _ =>
+                TerminalSet.subset lset (find_items_map items_map s2 prod (S pos))
+              | _ => false
+            end
+          | _ => false
+        end
+      | _ => true
+    end).
+
+Property is_terminal_shift_correct :
+  is_terminal_shift (items_map ()) = true -> terminal_shift.
+Proof.
+unfold is_terminal_shift, terminal_shift.
+intros.
+apply (forallb_items_spec _ H _ _ _ _ H0 (fun _ _ _ _ => _)).
+intros.
+destruct (future_of_prod prod0 pos) as [|[]] eqn:?; intuition.
+destruct (action_table st); intuition.
+destruct (l0 t); intuition.
+exists (S pos).
+split.
+unfold future_of_prod in *.
+rewrite Heql; reflexivity.
+apply (TerminalSet.subset_2 H2); intuition.
+Qed.
+
+(** If a state contains an item of the form A->_.[[a]], then either we do a
+    [Default_reduce_act] of the corresponding production, either a is a
+    terminal (ie. there is a lookahead terminal), and reading a does a
+    [Reduce_act] of the corresponding production. **)
+Definition end_reduce :=
+  forall (s:state) prod fut lookahead,
+    state_has_future s prod fut lookahead ->
+    fut = [] ->
+    match action_table s with
+      | Default_reduce_act p => p = prod
+      | Lookahead_act awt =>
+        match awt lookahead with
+          | Reduce_act p => p = prod
+          | _ => False
+        end
+    end.
+
+Definition is_end_reduce items_map :=
+  forallb_items items_map (fun s prod pos lset =>
+    match future_of_prod prod pos with
+      | [] =>
+        match action_table s with
+          | Default_reduce_act p => compare_eqb p prod
+          | Lookahead_act awt =>
+            TerminalSet.fold (fun lookahead acc =>
+              match awt lookahead with
+                | Reduce_act p => (acc && compare_eqb p prod)%bool
+                | _ => false
+              end) lset true
+        end
+        | _ => true
+      end).
+
+Property is_end_reduce_correct :
+  is_end_reduce (items_map ()) = true -> end_reduce.
+Proof.
+unfold is_end_reduce, end_reduce.
+intros.
+revert H1.
+apply (forallb_items_spec _ H _ _ _ _ H0 (fun _ _ _ _ => _)).
+intros.
+rewrite H3 in H2.
+destruct (action_table st); intuition.
+apply compare_eqb_iff; intuition.
+rewrite TerminalSet.fold_1 in H2.
+revert H2.
+generalize true at 1.
+pose proof (TerminalSet.elements_1 H1).
+induction H2.
+pose proof (compare_eq _ _ H2).
+destruct H4.
+simpl.
+assert (fold_left
+     (fun (a : bool) (e : TerminalSet.elt) =>
+       match l e with
+         | Shift_act _ _ => false
+         | Reduce_act p => (a && compare_eqb p prod0)%bool
+         | Fail_act => false
+       end) l0 false = true -> False).
+induction l0; intuition.
+apply IHl0.
+simpl in H4.
+destruct (l a); intuition.
+destruct (l lookahead0); intuition.
+apply compare_eqb_iff.
+destruct (compare_eqb p prod0); intuition.
+destruct b; intuition.
+simpl; intros.
+eapply IHInA; eauto.
+Qed.
+
+(** If a state contains an item of the form A->_.Bv[[b]], where B is a
+    non terminal, then the goto table says we have to go to a state containing
+    an item of the form A->_.v[[b]]. **)
+Definition non_terminal_goto :=
+  forall (s1:state) prod fut lookahead,
+    state_has_future s1 prod fut lookahead ->
+    match fut with
+      | NT nt::q =>
+        match goto_table s1 nt with
+          | Some (exist s2 _) =>
+            state_has_future s2 prod q lookahead
+          | None =>
+            forall prod fut lookahead,
+            state_has_future s1 prod fut lookahead ->
+            match fut with
+              | NT nt'::_ => nt <> nt'
+              | _ => True
+            end
+        end
+      | _ => True
+    end.
+
+Definition is_non_terminal_goto items_map :=
+  forallb_items items_map (fun s1 prod pos lset =>
+    match future_of_prod prod pos with
+      | NT nt::_ =>
+        match goto_table s1 nt with
+          | Some (exist s2 _) =>
+            TerminalSet.subset lset (find_items_map items_map s2 prod (S pos))
+          | None => forallb_items items_map (fun s1' prod' pos' _ =>
+            (implb (compare_eqb s1 s1')
+            match future_of_prod prod' pos' with
+              | NT nt' :: _ => negb (compare_eqb nt nt')
+              | _ => true
+            end)%bool)
+        end
+      | _ => true
+    end).
+
+Property is_non_terminal_goto_correct :
+  is_non_terminal_goto (items_map ()) = true -> non_terminal_goto.
+Proof.
+unfold is_non_terminal_goto, non_terminal_goto.
+intros.
+apply (forallb_items_spec _ H _ _ _ _ H0 (fun _ _ _ _ => _)).
+intros.
+destruct (future_of_prod prod0 pos) as [|[]] eqn:?; intuition.
+destruct (goto_table st n) as [[]|].
+exists (S pos).
+split.
+unfold future_of_prod in *.
+rewrite Heql; reflexivity.
+apply (TerminalSet.subset_2 H2); intuition.
+intros.
+remember st in H2; revert Heqs.
+apply (forallb_items_spec _ H2 _ _ _ _ H3 (fun _ _ _ _ => _)); intros.
+rewrite <- compare_eqb_iff in Heqs; rewrite Heqs in H5.
+destruct (future_of_prod prod2 pos0) as [|[]]; intuition.
+rewrite <- compare_eqb_iff in H6; rewrite H6 in H5.
+discriminate.
+Qed.
+
+Definition start_goto :=
+  forall (init:initstate), goto_table init (start_nt init) = None.
+
+Definition is_start_goto (_:unit) :=
+  forallb (fun (init:initstate) =>
+    match goto_table init (start_nt init) with
+      | Some _ => false
+      | None => true
+    end) all_list.
+
+Definition is_start_goto_correct:
+  is_start_goto () = true -> start_goto.
+Proof.
+unfold is_start_goto, start_goto.
+rewrite forallb_forall.
+intros.
+specialize (H init (all_list_forall _)).
+destruct (goto_table init (start_nt init)); congruence.
+Qed.
+
+(** Closure property of item sets : if a state contains an item of the form
+    A->_.Bv[[b]], then for each production B->u and each terminal a of
+    first(vb), the state contains an item of the form B->_.u[[a]] **)
+Definition non_terminal_closed :=
+  forall (s1:state) prod fut lookahead,
+    state_has_future s1 prod fut lookahead ->
+    match fut with
+      | NT nt::q =>
+        forall (p:production) (lookahead2:terminal),
+          prod_lhs p = nt ->
+          TerminalSet.In lookahead2 (first_word_set q) \/
+          lookahead2 = lookahead /\ nullable_word q = true ->
+            state_has_future s1 p (rev (prod_rhs_rev p)) lookahead2
+      | _ => True
+    end.
+
+Definition is_non_terminal_closed items_map :=
+  forallb_items items_map (fun s1 prod pos lset =>
+    match future_of_prod prod pos with
+        | NT nt::q =>
+          forallb (fun p =>
+            if compare_eqb (prod_lhs p) nt then
+              let lookaheads := find_items_map items_map s1 p 0 in
+              (implb (nullable_word q) (TerminalSet.subset lset lookaheads)) &&
+              TerminalSet.subset (first_word_set q) lookaheads
+            else true
+          )%bool all_list
+        | _ => true
+    end).
+
+Property is_non_terminal_closed_correct:
+  is_non_terminal_closed (items_map ()) = true -> non_terminal_closed.
+Proof.
+unfold is_non_terminal_closed, non_terminal_closed.
+intros.
+apply (forallb_items_spec _ H _ _ _ _ H0 (fun _ _ _ _ => _)).
+intros.
+destruct (future_of_prod prod0 pos); intuition.
+destruct s; eauto; intros.
+rewrite forallb_forall in H2.
+specialize (H2 p (all_list_forall p)).
+rewrite <- compare_eqb_iff in H3.
+rewrite H3 in H2.
+rewrite Bool.andb_true_iff in H2.
+destruct H2.
+exists 0.
+split.
+apply rev_alt.
+destruct H4 as [|[]]; subst.
+apply (TerminalSet.subset_2 H5); intuition.
+rewrite H6 in H2.
+apply (TerminalSet.subset_2 H2); intuition.
+Qed.
+
+(** The automaton is complete **)
+Definition complete :=
+  nullable_stable /\ first_stable /\ start_future /\ terminal_shift 
+  /\ end_reduce /\ non_terminal_goto /\ start_goto /\ non_terminal_closed.
+
+Definition is_complete (_:unit) :=
+  let items_map := items_map () in
+  (is_nullable_stable () && is_first_stable () && is_start_future items_map &&
+    is_terminal_shift items_map && is_end_reduce items_map && is_start_goto () &&
+    is_non_terminal_goto items_map && is_non_terminal_closed items_map)%bool.
+
+Property is_complete_correct:
+  is_complete () = true -> complete.
+Proof.
+unfold is_complete, complete.
+repeat rewrite Bool.andb_true_iff.
+intuition.
+apply is_nullable_stable_correct; assumption.
+apply is_first_stable_correct; assumption.
+apply is_start_future_correct; assumption.
+apply is_terminal_shift_correct; assumption.
+apply is_end_reduce_correct; assumption.
+apply is_non_terminal_goto_correct; assumption.
+apply is_start_goto_correct; assumption.
+apply is_non_terminal_closed_correct; assumption.
+Qed.
+
+End Make.
diff --git a/cparser/validator/Validator_safe.v b/cparser/validator/Validator_safe.v
new file mode 100644
index 0000000..119f733
--- /dev/null
+++ b/cparser/validator/Validator_safe.v
@@ -0,0 +1,414 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Jacques-Henri Jourdan, INRIA Paris-Rocquencourt            *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+Require Automaton.
+Require Import Alphabet.
+Require Import List.
+Require Import Syntax.
+
+Module Make(Import A:Automaton.T).
+
+(** The singleton predicate for states **)
+Definition singleton_state_pred (state:state) :=
+  (fun state' => match compare state state' with Eq => true |_ => false end).
+
+(** [past_state_of_non_init_state], extended for all states. **)
+Definition past_state_of_state (state:state) :=
+  match state with
+    | Init _ => []
+    | Ninit nis => past_state_of_non_init_state nis
+  end.
+
+(** Concatenations of last and past **)
+Definition head_symbs_of_state (state:state) :=
+  match state with
+    | Init _ => []
+    | Ninit s =>
+      last_symb_of_non_init_state s::past_symb_of_non_init_state s
+  end.
+Definition head_states_of_state (state:state) :=
+  singleton_state_pred state::past_state_of_state state.
+
+(** * Validation for correctness **)
+
+(** Prefix predicate between two lists of symbols. **)
+Inductive prefix: list symbol -> list symbol -> Prop :=
+  | prefix_nil: forall l, prefix [] l
+  | prefix_cons: forall l1 l2 x, prefix l1 l2 -> prefix (x::l1) (x::l2).
+
+Fixpoint is_prefix (l1 l2:list symbol):=
+  match l1, l2 with
+    | [], _ => true
+    | t1::q1, t2::q2 => (compare_eqb t1 t2 && is_prefix q1 q2)%bool
+    | _::_, [] => false
+  end.
+
+Property is_prefix_correct (l1 l2:list symbol):
+  is_prefix l1 l2 = true -> prefix l1 l2.
+Proof.
+revert l2.
+induction l1; intros.
+apply prefix_nil.
+unfold is_prefix in H.
+destruct l2; intuition; try discriminate.
+rewrite Bool.andb_true_iff in H.
+destruct H.
+rewrite compare_eqb_iff in H.
+destruct H.
+apply prefix_cons.
+apply IHl1; intuition.
+Qed.
+
+(** If we shift, then the known top symbols of the destination state is
+    a prefix of the known top symbols of the source state, with the new
+    symbol added. **)
+Definition shift_head_symbs :=
+  forall s,
+    match action_table s with
+      | Lookahead_act awp =>
+        forall t, match awp t with
+          | Shift_act s2 _ =>
+            prefix (past_symb_of_non_init_state s2) (head_symbs_of_state s)
+          | _ => True
+        end
+      | _ => True
+    end.
+
+Definition is_shift_head_symbs (_:unit) :=
+  forallb (fun s:state =>
+    match action_table s with
+      | Lookahead_act awp =>
+        forallb (fun t =>
+          match awp t with
+            | Shift_act s2 _ =>
+              is_prefix (past_symb_of_non_init_state s2) (head_symbs_of_state s)
+            | _ => true
+          end)
+          all_list
+      | _ => true
+    end)
+    all_list.
+
+Property is_shift_head_symbs_correct:
+  is_shift_head_symbs () = true -> shift_head_symbs.
+Proof.
+unfold is_shift_head_symbs, shift_head_symbs.
+intros.
+rewrite forallb_forall in H.
+specialize (H s (all_list_forall s)).
+destruct (action_table s); intuition.
+rewrite forallb_forall in H.
+specialize (H t (all_list_forall t)).
+destruct (l t); intuition.
+apply is_prefix_correct; intuition.
+Qed.
+
+(** When a goto happens, then the known top symbols of the destination state
+    is a prefix of the known top symbols of the source state, with the new
+    symbol added. **)
+Definition goto_head_symbs :=
+  forall s nt,
+    match goto_table s nt with
+      | Some (exist s2 _) => 
+        prefix (past_symb_of_non_init_state s2) (head_symbs_of_state s)
+      | None => True
+    end.
+
+Definition is_goto_head_symbs (_:unit) :=
+  forallb (fun s:state =>
+    forallb (fun nt =>
+      match goto_table s nt with
+        | Some (exist s2 _) =>
+          is_prefix (past_symb_of_non_init_state s2) (head_symbs_of_state s)
+        | None => true
+      end)
+      all_list)
+    all_list.
+
+Property is_goto_head_symbs_correct:
+  is_goto_head_symbs () = true -> goto_head_symbs.
+Proof.
+unfold is_goto_head_symbs, goto_head_symbs.
+intros.
+rewrite forallb_forall in H.
+specialize (H s (all_list_forall s)).
+rewrite forallb_forall in H.
+specialize (H nt (all_list_forall nt)).
+destruct (goto_table s nt); intuition.
+destruct s0.
+apply is_prefix_correct; intuition.
+Qed.
+
+(** We have to say the same kind of checks for the assumptions about the
+    states stack. However, theses assumptions are predicates. So we define
+    a notion of "prefix" over predicates lists, that means, basically, that
+    an assumption entails another **)
+Inductive prefix_pred: list (state->bool) -> list (state->bool) -> Prop :=
+  | prefix_pred_nil: forall l, prefix_pred [] l
+  | prefix_pred_cons: forall l1 l2 f1 f2,
+     (forall x, implb (f2 x) (f1 x) = true) ->
+     prefix_pred l1 l2 -> prefix_pred (f1::l1) (f2::l2).
+
+Fixpoint is_prefix_pred (l1 l2:list (state->bool)) :=
+  match l1, l2 with
+    | [], _ => true
+    | f1::q1, f2::q2 =>
+      (forallb (fun x => implb (f2 x) (f1 x)) all_list
+        && is_prefix_pred q1 q2)%bool
+    | _::_, [] => false
+  end.
+
+Property is_prefix_pred_correct (l1 l2:list (state->bool)) :
+  is_prefix_pred l1 l2 = true -> prefix_pred l1 l2.
+Proof.
+revert l2.
+induction l1.
+intros.
+apply prefix_pred_nil.
+intros.
+destruct l2; intuition; try discriminate.
+unfold is_prefix_pred in H.
+rewrite Bool.andb_true_iff in H.
+rewrite forallb_forall in H.
+apply prefix_pred_cons; intuition.
+apply H0.
+apply all_list_forall.
+Qed.
+
+(** The assumptions about state stack is conserved when we shift **)
+Definition shift_past_state :=
+  forall s,
+    match action_table s with
+      | Lookahead_act awp =>
+        forall t, match awp t with
+          | Shift_act s2 _ =>
+            prefix_pred (past_state_of_non_init_state s2)
+                        (head_states_of_state s)
+          | _ => True
+        end
+      | _ => True
+    end.
+
+Definition is_shift_past_state (_:unit) :=
+  forallb (fun s:state =>
+    match action_table s with
+      | Lookahead_act awp =>
+        forallb (fun t =>
+          match awp t with
+            | Shift_act s2 _ =>
+              is_prefix_pred
+                (past_state_of_non_init_state s2) (head_states_of_state s)
+            | _ => true
+          end)
+          all_list
+      | _ => true
+    end)
+    all_list.
+
+Property is_shift_past_state_correct:
+ is_shift_past_state () = true -> shift_past_state.
+Proof.
+unfold is_shift_past_state, shift_past_state.
+intros.
+rewrite forallb_forall in H.
+specialize (H s (all_list_forall s)).
+destruct (action_table s); intuition.
+rewrite forallb_forall in H.
+specialize (H t (all_list_forall t)).
+destruct (l t); intuition.
+apply is_prefix_pred_correct; intuition.
+Qed.
+
+(** The assumptions about state stack is conserved when we do a goto **)
+Definition goto_past_state :=
+  forall s nt,
+    match goto_table s nt with
+      | Some (exist s2 _) =>
+        prefix_pred (past_state_of_non_init_state s2)
+                    (head_states_of_state s)
+      | None => True
+    end.
+
+Definition is_goto_past_state (_:unit) :=
+  forallb (fun s:state =>
+    forallb (fun nt =>
+      match goto_table s nt with
+        | Some (exist s2 _) =>
+          is_prefix_pred
+            (past_state_of_non_init_state s2) (head_states_of_state s)
+        | None => true
+      end)
+      all_list)
+    all_list.
+
+Property is_goto_past_state_correct :
+  is_goto_past_state () = true -> goto_past_state.
+Proof.
+unfold is_goto_past_state, goto_past_state.
+intros.
+rewrite forallb_forall in H.
+specialize (H s (all_list_forall s)).
+rewrite forallb_forall in H.
+specialize (H nt (all_list_forall nt)).
+destruct (goto_table s nt); intuition.
+destruct s0.
+apply is_prefix_pred_correct; intuition.
+Qed.
+
+(** What states are possible after having popped these symbols from the
+    stack, given the annotation of the current state ? **)
+Inductive state_valid_after_pop (s:state):
+  list symbol -> list (state -> bool) -> Prop :=
+  | state_valid_after_pop_nil1:
+    forall p pl, p s = true -> state_valid_after_pop s [] (p::pl)
+  | state_valid_after_pop_nil2:
+    forall sl, state_valid_after_pop s sl []
+  | state_valid_after_pop_cons:
+    forall st sq p pl, state_valid_after_pop s sq pl ->
+      state_valid_after_pop s (st::sq) (p::pl).
+
+Fixpoint is_state_valid_after_pop
+  (state:state) (to_pop:list symbol) annot :=
+  match annot, to_pop with
+    | [], _ => true
+    | p::_, [] => p state
+    | p::pl, s::sl => is_state_valid_after_pop state sl pl
+  end.
+
+Property is_state_valid_after_pop_complete state sl pl :
+  state_valid_after_pop state sl pl -> is_state_valid_after_pop state sl pl = true.
+Proof.
+intro.
+induction H; intuition.
+destruct sl; intuition.
+Qed.
+
+(** A state is valid for reducing a production when :
+      - The assumptions on the state are such that we will find the right hand
+        side of the production on the stack.
+      - We will be able to do a goto after having popped the right hand side.
+**)
+Definition valid_for_reduce (state:state) prod :=
+    prefix (prod_rhs_rev prod) (head_symbs_of_state state) /\
+    forall state_new,
+    state_valid_after_pop state_new
+      (prod_rhs_rev prod) (head_states_of_state state) ->
+    goto_table state_new (prod_lhs prod) = None ->
+    match state_new with
+      | Init i => prod_lhs prod = start_nt i
+      | Ninit _ => False
+    end.
+
+Definition is_valid_for_reduce (state:state) prod:=
+  (is_prefix (prod_rhs_rev prod) (head_symbs_of_state state) &&
+   forallb (fun state_new =>
+     if is_state_valid_after_pop state_new (prod_rhs_rev prod)
+                                           (head_states_of_state state) then
+       match goto_table state_new (prod_lhs prod) with
+         | Some _ => true
+         | None =>
+           match state_new with
+             | Init i => compare_eqb (prod_lhs prod) (start_nt i)
+             | Ninit _ => false
+           end
+       end
+     else
+       true)
+     all_list)%bool.
+
+Property is_valid_for_reduce_correct (state:state) prod:
+  is_valid_for_reduce state prod = true -> valid_for_reduce state prod.
+Proof.
+unfold is_valid_for_reduce, valid_for_reduce.
+intros.
+rewrite Bool.andb_true_iff in H.
+split.
+apply is_prefix_correct.
+intuition.
+intros.
+rewrite forallb_forall in H.
+destruct H.
+specialize (H2 state_new (all_list_forall state_new)).
+rewrite is_state_valid_after_pop_complete, H1 in H2.
+destruct state_new; intuition.
+rewrite compare_eqb_iff in H2; intuition.
+intuition.
+Qed.
+
+(** All the states that does a reduce are valid for reduction **)
+Definition reduce_ok :=
+  forall s,
+    match action_table s with
+      | Lookahead_act awp =>
+        forall t, match awp t with
+          | Reduce_act p => valid_for_reduce s p
+          | _ => True
+        end
+      | Default_reduce_act p => valid_for_reduce s p
+    end.
+
+Definition is_reduce_ok (_:unit) :=
+  forallb (fun s =>
+    match action_table s with
+      | Lookahead_act awp =>
+        forallb (fun t =>
+          match awp t with
+            | Reduce_act p => is_valid_for_reduce s p
+            | _ => true
+          end)
+          all_list
+      | Default_reduce_act p => is_valid_for_reduce s p
+    end)
+    all_list.
+
+Property is_reduce_ok_correct :
+  is_reduce_ok () = true -> reduce_ok.
+Proof.
+unfold is_reduce_ok, reduce_ok.
+intros.
+rewrite forallb_forall in H.
+specialize (H s (all_list_forall s)).
+destruct (action_table s).
+apply is_valid_for_reduce_correct; intuition.
+intro.
+rewrite forallb_forall in H.
+specialize (H t (all_list_forall t)).
+destruct (l t); intuition.
+apply is_valid_for_reduce_correct; intuition.
+Qed.
+
+(** The automaton is safe **)
+Definition safe :=
+  shift_head_symbs /\ goto_head_symbs /\ shift_past_state /\
+  goto_past_state /\ reduce_ok.
+
+Definition is_safe (_:unit) :=
+  (is_shift_head_symbs () && is_goto_head_symbs () && is_shift_past_state () &&
+    is_goto_past_state () && is_reduce_ok ())%bool.
+
+Property is_safe_correct:
+  is_safe () = true -> safe.
+Proof.
+unfold safe, is_safe.
+repeat rewrite Bool.andb_true_iff.
+intuition.
+apply is_shift_head_symbs_correct; assumption.
+apply is_goto_head_symbs_correct; assumption.
+apply is_shift_past_state_correct; assumption.
+apply is_goto_past_state_correct; assumption.
+apply is_reduce_ok_correct; assumption.
+Qed.
+
+End Make.