More global initialization work done and proved in Coq.

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

3 files changed, 409 insertions, 79 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index eefc813..966bb76 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -23,6 +23,7 @@ open Camlcoq
 open AST
 open Values
 open Csyntax
+open Initializers
 
 (** Record the declarations of global variables and associate them
     with the corresponding atom. *)
@@ -745,75 +746,33 @@ let convertFundecl env (sto, id, ty, optinit) =
 
 (** Initializers *)
 
-let init_data_size = function
-  | Init_int8 _ -> 1
-  | Init_int16 _ -> 2
-  | Init_int32 _ -> 4
-  | Init_float32 _ -> 4
-  | Init_float64 _ -> 8
-  | Init_addrof _ -> 4
-  | Init_space _ -> assert false
-
 let string_of_errmsg msg =
   let string_of_err = function
   | CompcertErrors.MSG s -> camlstring_of_coqstring s
   | CompcertErrors.CTX i -> extern_atom i
   in String.concat "" (List.map string_of_err msg)
 
-let convertInit env ty init =
-
-  let k = ref []
-  and pos = ref 0 in
-  let emit size datum =
-    k := datum :: !k;
-    pos := !pos + size in
-  let emit_space size =
-    emit size (Init_space (z_of_camlint (Int32.of_int size))) in
-  let align size =
-    let n = !pos land (size - 1) in
-    if n > 0 then emit_space (size - n) in
-  let check_align size =
-    assert (!pos land (size - 1) = 0) in
-
-  let rec cvtInit ty = function
-  | Init_single e ->
-      begin match Initializers.transl_init_single
-                     (convertTyp env ty) (convertExpr env e) with
-      | CompcertErrors.OK init ->
-          let sz = init_data_size init in
-          check_align sz;
-          emit sz init
-      | CompcertErrors.Error msg ->
-          Format.printf "%a@." Cprint.exp (0, e);
-          error ("in initializing expression above: " ^ string_of_errmsg msg)
-      end
-  | Init_array il ->
-      let ty_elt =
-        match Cutil.unroll env ty with
-        | C.TArray(t, _, _) -> t
-        | _ -> error "array type expected in initializer"; C.TVoid [] in
-      List.iter (cvtInit ty_elt) il
-  | Init_struct(_, flds) ->
-      cvtPadToSizeof ty (fun () -> List.iter cvtFieldInit flds)
-  | Init_union(_, fld, i) ->
-      cvtPadToSizeof ty (fun () -> cvtFieldInit (fld,i))
-
-  and cvtFieldInit (fld, i) =
-    let ty' = convertTyp env fld.fld_typ in
-    let al = Int32.to_int (camlint_of_z (Csyntax.alignof ty')) in
-    align al;
-    cvtInit fld.fld_typ i
-
-  and cvtPadToSizeof ty fn =
-    let ty' = convertTyp env ty in
-    let sz = Int32.to_int (camlint_of_z (Csyntax.sizeof ty')) in
-    let pos0 = !pos in
-    fn();
-    let pos1 = !pos in
-    assert (pos1 <= pos0 + sz);
-    if pos1 < pos0 + sz then emit_space (pos0 + sz - pos1)
-
-  in cvtInit ty init; List.rev !k
+let rec convertInit env init =
+  match init with
+  | C.Init_single e ->
+      Init_single (convertExpr env e)
+  | C.Init_array il ->
+      Init_compound (convertInitList env il)
+  | C.Init_struct(_, flds) ->
+      Init_compound (convertInitList env (List.map snd flds))
+  | C.Init_union(_, fld, i) ->
+      Init_compound (Init_cons(convertInit env i, Init_nil))
+
+and convertInitList env il =
+  match il with
+  | [] -> Init_nil
+  | i :: il' -> Init_cons(convertInit env i, convertInitList env il')
+
+let convertInitializer env ty i =
+  match Initializers.transl_init (convertTyp env ty) (convertInit env i)
+  with
+  | CompcertErrors.OK init -> init
+  | CompcertErrors.Error msg -> error (string_of_errmsg msg); []
 
 (** Global variable *)
 
@@ -840,7 +799,7 @@ let convertGlobvar env (sto, id, ty, optinit) =
     | None ->
         if sto = C.Storage_extern then [] else [Init_space(Csyntax.sizeof ty')]
     | Some i ->
-        convertInit env ty i in
+        convertInitializer env ty i in
   Hashtbl.add decl_atom id'
     { a_storage = sto;
       a_env = env;
diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v
index 926a826..5df8243 100644
--- a/cfrontend/Initializers.v
+++ b/cfrontend/Initializers.v
@@ -149,8 +149,15 @@ Fixpoint constval (a: expr) : res val :=
 
 (** * Translation of initializers *)
 
+Inductive initializer :=
+  | Init_single (a: expr)
+  | Init_compound (il: initializer_list)
+with initializer_list :=
+  | Init_nil
+  | Init_cons (i: initializer) (il: initializer_list).
+
 (** Translate an initializing expression [a] for a scalar variable
-  of type [ty].  Return the corresponding [init_data]. *)
+  of type [ty].  Return the corresponding initialization datum. *)
 
 Definition transl_init_single (ty: type) (a: expr) : res init_data :=
   do v1 <- constval a;
@@ -168,6 +175,70 @@ Definition transl_init_single (ty: type) (a: expr) : res init_data :=
   | _, _ => Error (msg "type mismatch in initializer")
   end.
 
-(** To come later: translation of compound initializers, currently
-  still done in Caml (module [C2C]). *)
+(** Translate an initializer [i] for a variable of type [ty].
+  Return the corresponding list of initialization data. *)
+
+Definition padding (frm to: Z) : list init_data :=
+  let n := to - frm in
+  if zle n 0 then nil else Init_space n :: nil.
+
+Fixpoint transl_init (ty: type) (i: initializer)
+                     {struct i} : res (list init_data) :=
+  match i, ty with
+  | Init_single a, _ =>
+      do d <- transl_init_single ty a; OK (d :: nil)
+  | Init_compound il, Tarray tyelt sz =>
+      if zle sz 0
+      then OK (Init_space(sizeof tyelt) :: nil)
+      else transl_init_array tyelt il sz
+  | Init_compound il, Tstruct _ Fnil =>
+      OK (Init_space (sizeof ty) :: nil)
+  | Init_compound il, Tstruct id fl =>
+      transl_init_struct id ty fl il 0
+  | Init_compound il, Tunion _ Fnil =>
+      OK (Init_space (sizeof ty) :: nil)
+  | Init_compound il, Tunion id (Fcons _ ty1 _) =>
+      transl_init_union id ty ty1 il
+  | _, _ =>
+      Error (msg "wrong type for compound initializer")
+  end
+
+with transl_init_array (ty: type) (il: initializer_list) (sz: Z)
+                       {struct il} : res (list init_data) :=
+  match il with
+  | Init_nil =>
+      if zeq sz 0
+      then OK nil
+      else Error (msg "wrong number of elements in array initializer")
+  | Init_cons i1 il' =>
+      do d1 <- transl_init ty i1;
+      do d2 <- transl_init_array ty il' (sz - 1);
+      OK (d1 ++ d2)
+  end
+
+with transl_init_struct (id: ident) (ty: type)
+                        (fl: fieldlist) (il: initializer_list) (pos: Z)
+                        {struct il} : res (list init_data) :=
+  match il, fl with
+  | Init_nil, Fnil =>
+      OK (padding pos (sizeof ty))
+  | Init_cons i1 il', Fcons _ ty1 fl' =>
+      let pos1 := align pos (alignof ty1) in
+      do d1 <- transl_init (unroll_composite id ty ty1) i1;
+      do d2 <- transl_init_struct id ty fl' il' (pos1 + sizeof ty1);
+      OK (padding pos pos1 ++ d1 ++ d2)
+  | _, _ =>
+      Error (msg "wrong number of elements in struct initializer")
+  end
+
+with transl_init_union (id: ident) (ty ty1: type) (il: initializer_list)
+                       {struct il} : res (list init_data) :=
+  match il with
+  | Init_nil =>
+      Error (msg "empty union initializer")
+  | Init_cons i1 _ =>
+      do d <- transl_init (unroll_composite id ty ty1) i1;
+      OK (d ++ padding (sizeof ty1) (sizeof ty))
+  end.
+
 
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index fde3c4e..2bc4b7c 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -520,36 +520,336 @@ Qed.
 
 (** * Soundness of the translation of initializers *)
 
+(** Soundness for single initializers. *)
+
 Theorem transl_init_single_steps:
-  forall ty a data f m w v1 ty1 m' v b ofs m'',
+  forall ty a data f m w v1 ty1 m' v chunk b ofs m'',
   transl_init_single ty a = OK data ->
   star step ge (ExprState f a Kstop empty_env m) w (ExprState f (Eval v1 ty1) Kstop empty_env m') ->
   cast v1 ty1 ty v ->
-  store_value_of_type ty m' b ofs v = Some m'' ->
-  Genv.store_init_data ge m b (Int.signed ofs) data = Some m''.
+  access_mode ty = By_value chunk ->
+  Mem.store chunk m' b ofs v = Some m'' ->
+  Genv.store_init_data ge m b ofs data = Some m''.
 Proof.
   intros. monadInv H. 
   exploit constval_steps; eauto. intros [A [B C]]. subst m' ty1.
   exploit cast_match; eauto. intros D.
-  unfold Genv.store_init_data. unfold store_value_of_type in H2. simpl in H2. 
+  unfold Genv.store_init_data. 
   inv D. 
   (* int *)
   destruct ty; try discriminate. 
   destruct i; inv EQ2.
-  destruct s; simpl in H2. rewrite <- Mem.store_signed_unsigned_8; auto. auto. 
-  destruct s; simpl in H2. rewrite <- Mem.store_signed_unsigned_16; auto. auto.
-  assumption.
-  inv EQ2. assumption.
+  destruct s; simpl in H2; inv H2. rewrite <- Mem.store_signed_unsigned_8; auto. auto.
+  destruct s; simpl in H2; inv H2. rewrite <- Mem.store_signed_unsigned_16; auto. auto.
+  simpl in H2; inv H2. assumption.
+  inv EQ2. simpl in H2; inv H2. assumption.
   (* float *)
   destruct ty; try discriminate. 
-  destruct f1; inv EQ2; assumption.
+  destruct f1; inv EQ2; simpl in H2; inv H2; assumption.
   (* pointer *)
-  assert (data = Init_addrof id ofs0 /\ access_mode ty = By_value Mint32).
-    destruct ty; inv EQ2; auto. destruct i; inv H4; auto.
-  destruct H3; subst. rewrite H4 in H2. rewrite H. assumption.
+  assert (data = Init_addrof id ofs0 /\ chunk = Mint32).
+    destruct ty; inv EQ2; inv H2. destruct i; inv H5. intuition congruence. auto.
+  destruct H4; subst. rewrite H. assumption.
   (* undef *)
   discriminate.
 Qed.
 
+(** Size properties for initializers. *)
+
+Lemma transl_init_single_size:
+  forall ty a data,
+  transl_init_single ty a = OK data ->
+  Genv.init_data_size data = sizeof ty.
+Proof.
+  intros. monadInv H. destruct x0. 
+  monadInv EQ2.
+  destruct ty; try discriminate. 
+  destruct i0; inv EQ2; reflexivity.
+  inv EQ2; reflexivity.
+  destruct ty; try discriminate.
+  destruct f0; inv EQ2; reflexivity.
+  destruct b; try discriminate.
+  destruct ty; try discriminate.
+  destruct i0; inv EQ2; reflexivity.
+  inv EQ2; reflexivity.
+Qed.
+
+Notation idlsize := Genv.init_data_list_size.
+
+Remark padding_size:
+  forall frm to,
+  frm <= to -> idlsize (padding frm to) = to - frm.
+Proof.
+  intros. unfold padding. 
+  destruct (zle (to - frm) 0). 
+  simpl. omega.
+  simpl. rewrite Zmax_spec. rewrite zlt_true. omega. omega.
+Qed. 
+
+Remark idlsize_app:
+  forall d1 d2, idlsize (d1 ++ d2) = idlsize d1 + idlsize d2.
+Proof.
+  induction d1; simpl; intros. 
+  auto.
+  rewrite IHd1. omega.
+Qed.
+
+Remark sizeof_struct_incr:
+  forall fl pos, pos <= sizeof_struct fl pos.
+Proof.
+  induction fl; intros; simpl. 
+  omega.
+  eapply Zle_trans. apply align_le with (y := alignof t). apply alignof_pos.
+  eapply Zle_trans. 2: apply IHfl.
+  generalize (sizeof_pos t); omega.
+Qed.
+
+Remark sizeof_struct_eq:
+  forall id fl,
+  fl <> Fnil ->
+  sizeof (Tstruct id fl) = align (sizeof_struct fl 0) (alignof (Tstruct id fl)).
+Proof.
+  intros. simpl. f_equal. rewrite Zmax_spec. apply zlt_false. 
+  destruct fl. congruence. simpl. 
+  apply Zle_ge. eapply Zle_trans. 2: apply sizeof_struct_incr. 
+  assert (0 <= align 0 (alignof t)). apply align_le. apply alignof_pos. 
+  generalize (sizeof_pos t). omega.
+Qed.
+
+Remark sizeof_union_eq:
+  forall id fl,
+  fl <> Fnil ->
+  sizeof (Tunion id fl) = align (sizeof_union fl) (alignof (Tunion id fl)).
+Proof.
+  intros. simpl. f_equal. rewrite Zmax_spec. apply zlt_false. 
+  destruct fl. congruence. simpl. 
+  apply Zle_ge. apply Zmax_bound_l. generalize (sizeof_pos t). omega.
+Qed.
+
+Lemma transl_init_size:
+  forall i ty data,
+  transl_init ty i = OK data ->
+  idlsize data = sizeof ty
+
+with transl_init_list_size:
+  forall il,
+  (forall ty sz data,
+   transl_init_array ty il sz = OK data ->
+   idlsize data = sizeof ty * sz)
+  /\
+  (forall id ty fl pos data,
+   transl_init_struct id ty fl il pos = OK data ->
+   sizeof_struct fl pos <= sizeof ty ->
+   idlsize data + pos = sizeof ty)
+  /\
+  (forall id ty ty1 data,
+   transl_init_union id ty ty1 il = OK data ->
+   sizeof ty1 <= sizeof ty ->
+   idlsize data = sizeof ty).
+
+Proof.
+  induction i; intros. 
+  (* single *)
+  monadInv H. simpl. rewrite (transl_init_single_size _ _ _ EQ). omega.
+  (* compound *)
+  simpl in H. destruct ty; try discriminate.
+  (* compound array *)
+  destruct (zle z 0). 
+  monadInv H. simpl. repeat rewrite Zmax_spec. rewrite zlt_true. rewrite zlt_true. ring.
+  omega. generalize (sizeof_pos ty); omega.
+  simpl. rewrite Zmax_spec. rewrite zlt_false.
+  eapply (proj1 (transl_init_list_size il)). auto. omega.
+  (* compound struct *)
+  destruct f. 
+  inv H. reflexivity.
+  replace (idlsize data) with (idlsize data + 0) by omega.
+  eapply (proj1 (proj2 (transl_init_list_size il))). eauto.
+  rewrite sizeof_struct_eq. 2: congruence. 
+  apply align_le. apply alignof_pos.
+  (* compound union *)
+  destruct f.
+  inv H. reflexivity.
+  eapply (proj2 (proj2 (transl_init_list_size il))). eauto. 
+  rewrite sizeof_union_eq. 2: congruence. 
+  eapply Zle_trans. 2: apply align_le. simpl. apply Zmax_bound_l. omega. 
+  apply alignof_pos.
+
+  induction il.
+  (* base cases *)
+  simpl. intuition. 
+  (* arrays *)
+  destruct (zeq sz 0); inv H. simpl. ring. 
+  (* structs *)
+  destruct fl; inv H.
+  simpl in H0. generalize (padding_size pos (sizeof ty) H0). omega.
+  (* unions *)
+  inv H.
+  (* inductive cases *)
+  destruct IHil as [A [B C]]. split.
+  (* arrays *)
+  intros. monadInv H.
+  rewrite idlsize_app. 
+  rewrite (transl_init_size _ _ _ EQ). 
+  rewrite (A _ _ _ EQ1).
+  ring.
+  (* structs *)
+  split. intros. simpl in H. destruct fl; monadInv H.
+  repeat rewrite idlsize_app. 
+  simpl in H0. 
+  rewrite padding_size.
+  rewrite (transl_init_size _ _ _ EQ). rewrite sizeof_unroll_composite.
+  rewrite <- (B _ _ _ _ _ EQ1). omega.
+  auto. apply align_le. apply alignof_pos. 
+  (* unions *)
+  intros. simpl in H. monadInv H. 
+  rewrite idlsize_app.
+  rewrite (transl_init_size _ _ _ EQ). rewrite sizeof_unroll_composite. 
+  rewrite padding_size. omega. auto.
+Qed.
+
+(** A semantics for general initializers *)
+
+Definition dummy_function := mkfunction Tvoid nil nil Sskip.
+
+Require Import Events.
+
+Fixpoint fieldlist_map (f: type -> type) (l: fieldlist) : fieldlist :=
+  match l with
+  | Fnil => Fnil
+  | Fcons id ty l' => Fcons id (f ty) (fieldlist_map f l')
+  end.
+
+Inductive exec_init: mem -> block -> Z -> type -> initializer -> mem -> Prop :=
+  | exec_init_single: forall m b ofs ty a v1 ty1 chunk m' v m'',
+      star step ge (ExprState dummy_function a Kstop empty_env m) 
+                E0 (ExprState dummy_function (Eval v1 ty1) Kstop empty_env m') ->
+      cast v1 ty1 ty v ->
+      access_mode ty = By_value chunk ->
+      Mem.store chunk m' b ofs v = Some m'' ->
+      exec_init m b ofs ty (Init_single a) m''
+  | exec_init_compound_array: forall m b ofs ty sz il m',
+      exec_init_array m b ofs ty sz il m' ->
+      exec_init m b ofs (Tarray ty sz) (Init_compound il) m'
+  | exec_init_compound_struct: forall m b ofs id fl il m',
+      exec_init_struct m b ofs 0 (fieldlist_map (unroll_composite id (Tstruct id fl)) fl) il m' ->
+      exec_init m b ofs (Tstruct id fl) (Init_compound il) m'
+  | exec_init_compound_union: forall m b ofs id id1 ty1 fl i m',
+      exec_init m b ofs (unroll_composite id (Tunion id (Fcons id1 ty1 fl)) ty1) i m' ->
+      exec_init m b ofs (Tunion id (Fcons id1 ty1 fl)) (Init_compound (Init_cons i Init_nil)) m'
+
+with exec_init_array: mem -> block -> Z -> type -> Z -> initializer_list -> mem -> Prop :=
+  | exec_init_array_nil: forall m b ofs ty,
+      exec_init_array m b ofs ty 0 Init_nil m
+  | exec_init_array_cons: forall m b ofs ty sz i1 il m' m'',
+      exec_init m b ofs ty i1 m' ->
+      exec_init_array m' b (ofs + sizeof ty) ty (sz - 1) il m'' ->
+      exec_init_array m b ofs ty sz (Init_cons i1 il) m''
+
+with exec_init_struct: mem -> block -> Z -> Z -> fieldlist -> initializer_list -> mem -> Prop :=
+  | exec_init_struct_nil: forall m b ofs pos,
+      exec_init_struct m b ofs pos Fnil Init_nil m
+  | exec_init_struct_cons: forall m b ofs pos id ty fl i1 il m' m'',
+      exec_init m b (ofs + align pos (alignof ty)) ty i1 m' ->
+      exec_init_struct m' b ofs (align pos (alignof ty) + sizeof ty) fl il m'' ->
+      exec_init_struct m b ofs pos (Fcons id ty fl) (Init_cons i1 il) m''.
+
+Scheme exec_init_ind3 := Minimality for exec_init Sort Prop
+  with exec_init_array_ind3 := Minimality for exec_init_array Sort Prop
+  with exec_init_struct_ind3 := Minimality for exec_init_struct Sort Prop.
+Combined Scheme exec_init_scheme from exec_init_ind3, exec_init_array_ind3, exec_init_struct_ind3.
+
+Remark exec_init_array_length:
+  forall m b ofs ty sz il m', 
+  exec_init_array m b ofs ty sz il m' ->
+  match il with Init_nil => sz = 0 | Init_cons _ _ => sz > 0 end.
+Proof.
+  induction 1. auto. destruct il; omega. 
+Qed.
+
+Lemma store_init_data_list_app:
+  forall data1 m b ofs m' data2 m'',
+  Genv.store_init_data_list ge m b ofs data1 = Some m' ->
+  Genv.store_init_data_list ge m' b (ofs + idlsize data1) data2 = Some m'' ->
+  Genv.store_init_data_list ge m b ofs (data1 ++ data2) = Some m''.
+Proof.
+  induction data1; simpl; intros. 
+  inv H. rewrite Zplus_0_r in H0. auto.
+  destruct (Genv.store_init_data ge m b ofs a); try discriminate.
+  rewrite Zplus_assoc in H0. eauto.
+Qed.
+
+Remark store_init_data_list_padding:
+  forall frm to b ofs m,
+  Genv.store_init_data_list ge m b ofs (padding frm to) = Some m.
+Proof.
+  intros. unfold padding. destruct (zle (to - frm) 0); auto.
+Qed.
+
+Lemma transl_init_sound_gen:
+  (forall m b ofs ty i m', exec_init m b ofs ty i m' ->
+   forall data, transl_init ty i = OK data ->
+   Genv.store_init_data_list ge m b ofs data = Some m')
+/\(forall m b ofs ty sz il m', exec_init_array m b ofs ty sz il m' ->
+   forall data, transl_init_array ty il sz = OK data ->
+   Genv.store_init_data_list ge m b ofs data = Some m')
+/\(forall m b ofs pos fl il m', exec_init_struct m b ofs pos fl il m' ->
+   forall id ty fl' data,
+   fl = fieldlist_map (unroll_composite id ty) fl' ->
+   transl_init_struct id ty fl' il pos = OK data ->
+   Genv.store_init_data_list ge m b (ofs + pos) data = Some m').
+Proof.
+  apply exec_init_scheme; simpl; intros.
+  (* single *)
+  monadInv H3.
+  exploit transl_init_single_steps; eauto. intros. 
+  simpl. rewrite H3. auto.
+  (* array *)
+  destruct (zle sz 0).
+  exploit exec_init_array_length; eauto. destruct il; intros.
+  subst. inv H. inv H1. auto. omegaContradiction.
+  eauto.
+  (* struct *)
+  destruct fl.
+  inv H. inv H1. auto. 
+  replace ofs with (ofs + 0) by omega. eauto.
+  (* union *)
+  monadInv H1. eapply store_init_data_list_app. eauto. apply store_init_data_list_padding. 
+
+  (* array, empty *)
+  inv H. auto.
+  (* array, nonempty *)
+  monadInv H3. 
+  eapply store_init_data_list_app.
+  eauto.
+  rewrite (transl_init_size _ _ _ EQ). eauto.
+
+  (* struct, empty *)
+  destruct fl'; simpl in H; inv H. 
+  inv H0. apply store_init_data_list_padding.
+  (* struct, nonempty *)
+  destruct fl'; simpl in H3; inv H3.
+  monadInv H4. 
+  eapply store_init_data_list_app. apply store_init_data_list_padding.
+  rewrite padding_size. 
+  replace (ofs + pos + (align pos (alignof t) - pos))
+     with (ofs + align pos (alignof t)) by omega.
+  eapply store_init_data_list_app.
+  rewrite <- (alignof_unroll_composite id0 ty0 t).
+  eauto.
+  rewrite (transl_init_size _ _ _ EQ).
+  rewrite <- Zplus_assoc. rewrite <- (alignof_unroll_composite id0 ty0 t). 
+  eapply H2. eauto. rewrite alignof_unroll_composite. rewrite sizeof_unroll_composite. eauto.
+  apply align_le. apply alignof_pos.
+Qed.
+
+Theorem transl_init_sound:
+  forall m b ty i m' data,
+  exec_init m b 0 ty i m' ->
+  transl_init ty i = OK data ->
+  Genv.store_init_data_list ge m b 0 data = Some m'.
+Proof.
+  intros. eapply (proj1 transl_init_sound_gen); eauto.
+Qed.
+
 End SOUNDNESS.