Merge pull request #37 from WasmCert/inst_typing_compute

Computable version of inst_typing, and some associated fixes for cl_typing

Author: raoxiaojia

theories/context_inference.v

@@ -0,0 +1,214 @@
+From mathcomp Require Import ssreflect ssrfun ssrnat ssrbool eqtype seq.
+From compcert Require lib.Floats.
+From Wasm Require Export common typing operations.
+From Coq Require Import BinNat.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Section Context_inference.
+
+Variable host_function : eqType.
+
+Let function_closure := function_closure host_function.
+Let store_record := store_record host_function.
+
+Definition func_typing_inf (fs: list function_closure) (n: nat) : option function_type :=
+  option_map cl_type (List.nth_error fs n).
+
+Definition funcs_typing_inf (s: store_record) (inst: instance) : option (list function_type) :=
+  those (map (fun i => func_typing_inf s.(s_funcs) i) inst.(inst_funcs)).
+
+(* Choosing the most lenient bound *)
+Definition tab_typing_inf (ts: list tableinst) (n: nat) : option table_type :=
+  match List.nth_error ts n with
+  | Some _ => Some (Build_table_type (Build_limits 0%N None) ELT_funcref)
+  | _ => None
+  end.
+
+Definition tabs_typing_inf (s: store_record) (inst: instance) : option (list table_type) :=
+  those (map (fun i => tab_typing_inf s.(s_tables) i) inst.(inst_tab)).
+
+(* Choosing the most lenient bound *)
+Definition mem_typing_inf (ms: list memory) (n: nat) : option memory_type :=
+  match List.nth_error ms n with
+  | Some _ => Some (Build_limits 0%N None)
+  | _ => None
+  end.
+
+Definition mems_typing_inf (s: store_record) (inst: instance) : option (list memory_type) :=
+  those (map (fun i => mem_typing_inf s.(s_mems) i) inst.(inst_memory)).
+
+Definition global_typing_inf (gs: list global) (n: nat) : option global_type :=
+  match List.nth_error gs n with
+  | Some g => Some (Build_global_type g.(g_mut) (typeof g.(g_val)))
+  | _ => None
+  end.
+
+Definition globals_typing_inf (s: store_record) (inst: instance) : option (list global_type) :=
+  those (map (fun i => global_typing_inf s.(s_globals) i) inst.(inst_globs)).
+
+Definition inst_typing_inf (s: store_record) (inst: instance) : option t_context :=
+  match funcs_typing_inf s inst with
+  | Some fts =>
+      match tabs_typing_inf s inst with
+      | Some tts =>
+          match mems_typing_inf s inst with
+          | Some mts =>
+              match globals_typing_inf s inst with
+              | Some gts =>
+                  Some (Build_t_context inst.(inst_types) fts gts tts mts nil nil None)
+              | _ => None
+              end
+          | _ => None
+          end
+      | _ => None
+      end
+  | _ => None
+  end.
+
+Definition frame_typing_inf (s: store_record) (f: frame) : option t_context :=
+  match inst_typing_inf s f.(f_inst) with
+  | Some C => Some (upd_local C ((map typeof f.(f_locs)) ++ tc_local C))
+  | None => None
+  end.
+
+Lemma func_typing_inf_agree: forall xs n x,
+    (func_typing_inf xs n == Some x) = 
+      functions_agree xs n x.
+Proof.
+  move => xs n x.
+  unfold func_typing_inf, functions_agree.
+  destruct (List.nth_error xs n) as [ x' | ] eqn:Hnth; rewrite Hnth => /=.
+  - assert (n < length xs)%coq_nat as Hlen; first by apply List.nth_error_Some; rewrite Hnth.
+    move/ltP in Hlen.
+    by rewrite Hlen.
+  - cbn.
+    by lias.
+Qed.
+
+Lemma tab_typing_inf_agree: forall xs n x,
+    tab_typing_inf xs n = Some x ->
+    tabi_agree xs n x.
+Proof.
+  move => xs n x.
+  unfold tab_typing_inf, tabi_agree, tab_typing, limit_match.
+  destruct (List.nth_error xs n) as [ x' | ] eqn:Hnth => //=.
+  assert (n < length xs)%coq_nat as Hlen; first by apply List.nth_error_Some; rewrite Hnth.
+  move => Hinf.
+  move/ltP in Hlen.
+  rewrite Hlen => /=.
+  injection Hinf as <-.
+  cbn.
+  rewrite Bool.andb_true_r.
+  apply/N.leb_spec0.
+  by lias.
+Qed.
+
+Lemma mem_typing_inf_agree: forall xs n x,
+    mem_typing_inf xs n = Some x ->
+    memi_agree xs n x.
+Proof.
+  move => xs n x.
+  unfold mem_typing_inf, memi_agree, mem_typing, limit_match.
+  destruct (List.nth_error xs n) as [ x' | ] eqn:Hnth => //=.
+  assert (n < length xs)%coq_nat as Hlen; first by apply List.nth_error_Some; rewrite Hnth.
+  move => Hinf.
+  move/ltP in Hlen.
+  rewrite Hlen => /=.
+  injection Hinf as <-.
+  cbn.
+  rewrite Bool.andb_true_r.
+  apply/N.leb_spec0.
+  by lias.
+Qed.
+
+Lemma global_typing_inf_agree: forall xs n x,
+    (global_typing_inf xs n = Some x) ->
+    globals_agree xs n x.
+Proof.
+  move => xs n x.
+  unfold global_typing_inf, globals_agree, global_agree.
+  destruct (List.nth_error xs n) as [ x' | ] eqn:Hnth => //=.
+  assert (n < length xs)%coq_nat as Hlen; first by apply List.nth_error_Some; rewrite Hnth.
+    move/ltP in Hlen.
+    rewrite Hlen => /=.
+    move => [<-] => /=.
+    apply/eqP; f_equal.
+    by lias.
+Qed.
+
+Lemma those_all2_impl {X Y Z: Type}: forall (xs: list X) (ns: list Y) (ts: list Z) (f: list X -> Y -> option Z) (g: list X -> Y -> Z -> bool),
+    (forall xs n x, f xs n = Some x -> g xs n x) ->
+    (those (map (f xs) ns) = Some ts) ->
+    all2 (g xs) ns ts.
+Proof.
+  setoid_rewrite <- those_those0.
+  move => xs.
+  elim => //=; first by intros; destruct ts.
+  move => y ys IH ts f g Heq Himpl.
+  remove_bools_options.
+  apply Heq in Hoption.
+  eapply IH in Hoption0; last by apply Heq.
+  by rewrite Hoption Hoption0.
+Qed.
+  
+Lemma funcs_typing_inf_agree: forall s inst xts,
+  (funcs_typing_inf s inst = Some xts) ->
+  all2 (functions_agree s.(s_funcs)) inst.(inst_funcs) xts.
+Proof.
+  move => f inst xts Hinf.
+  unfold funcs_typing_inf in Hinf.
+  eapply those_all2_impl; eauto.
+  intros.
+  rewrite <- func_typing_inf_agree.
+  by apply/eqP.
+Qed.
+
+Lemma tabs_typing_inf_agree: forall s inst xts,
+  (tabs_typing_inf s inst = Some xts) ->
+  all2 (tabi_agree s.(s_tables)) inst.(inst_tab) xts.
+Proof.
+  move => f inst fts Hinf.
+  eapply those_all2_impl; eauto.
+  intros.
+  by apply tab_typing_inf_agree.
+Qed.
+
+Lemma mems_typing_inf_agree: forall s inst xts,
+  (mems_typing_inf s inst = Some xts) ->
+  all2 (memi_agree s.(s_mems)) inst.(inst_memory) xts.
+Proof.
+  move => f inst fts Hinf.
+  eapply those_all2_impl; eauto.
+  intros.
+  by apply mem_typing_inf_agree.
+Qed.
+
+Lemma globals_typing_inf_agree: forall s inst xts,
+  (globals_typing_inf s inst = Some xts) ->
+  all2 (globals_agree s.(s_globals)) inst.(inst_globs) xts.
+Proof.
+  move => f inst fts Hinf.
+  eapply those_all2_impl; eauto.
+  intros.
+  by apply global_typing_inf_agree.
+Qed.
+
+Lemma inst_typing_inf_impl: forall s inst C,
+    inst_typing_inf s inst = Some C ->
+    inst_typing s inst C.
+Proof.
+  move => s inst C Hinf.
+  unfold inst_typing_inf in Hinf.
+  destruct inst.
+  remove_bools_options => /=.
+  apply/andP; split; last by apply mems_typing_inf_agree in Hoption1.
+  apply/andP; split; last by apply tabs_typing_inf_agree in Hoption0.
+  apply/andP; split; last by apply globals_typing_inf_agree in Hoption2.
+  apply/andP; split; last by apply funcs_typing_inf_agree in Hoption.
+  by apply/eqP.
+Defined.
+  
+End Context_inference.

theories/instantiation_sound.v

@@ -92,7 +92,6 @@ Proof.
     by rewrite -> H.
 Qed.
 
-
 Let cl_type_check_single := @cl_type_check_single host_function.
 
 Lemma cl_type_check_single_aux s_funcs s_tables s_mems s_globals func funcs tabs mems globs:
@@ -111,7 +110,7 @@ Proof.
     rename H4 into Hinst_typing. rename H8 into Hbe_typing.
     apply cl_typing_native
       with (C := C)
-           (C' := upd_local_label_return C (tc_local C ++ t1s ++ ts) ([::t2s] ++ tc_label C) (Some t2s))
+           (C' := upd_local_label_return C (t1s ++ ts) ([::t2s]) (Some t2s))
           => //=.
     destruct C.
     rewrite /inst_typing. simpl.
@@ -630,10 +629,10 @@ Proof.
      this is no longer true in the future. *)
   exists (ET_tab {| tt_limits := {| lim_min := N.of_nat (tab_size tab); lim_max := table_max_opt tab |} ; tt_elem_type := ELT_funcref |}).
   econstructor; eauto.
-  unfold tab_typing => /=.
-  apply/andP; split => //.
-  rewrite nat_bin.
-  by lias.
+  unfold tab_typing, limit_match => /=.
+  apply/andP; split => //=; first by apply/N.leb_spec0; lias.
+  destruct (table_max_opt tab) eqn:Hopt => //.
+  by apply/N.leb_spec0; lias.
 Qed.
 
 Lemma ext_typing_exists_mem addr s:
@@ -648,12 +647,12 @@ Proof.
   destruct Hnth as [mem Hnth].
 
   (* Similar to tab_typing *)
-  exists (ET_mem {| lim_min := N.of_nat (mem_size mem); lim_max := mem_max_opt mem |}).
+  exists (ET_mem {| lim_min := mem_size mem; lim_max := mem_max_opt mem |}).
   econstructor; eauto.
-  unfold mem_typing => /=.
-  apply/andP; split => //.
-  rewrite nat_bin N2Nat.id.
-  by apply N.leb_refl.
+  unfold mem_typing, limit_match => /=.
+  apply/andP; split => //=; first by apply/N.leb_spec0; lias.
+  destruct (mem_max_opt mem) eqn:Hopt => //.
+  by apply/N.leb_spec0; lias.
 Qed.
 
 Lemma ext_typing_exists_glob addr s:
@@ -667,8 +666,6 @@ Proof.
     apply nth_error_Some in Hnth'; by lias. }
   destruct Hnth as [glob Hnth].
 
-  (* Note that all tables can be tab_typed. This lemma needs more information if
-     this is no longer true in the future. *)
   exists (ET_glob {| tg_mut := g_mut glob; tg_t := typeof (g_val glob) |}).
   econstructor; eauto.
   unfold global_agree => /=.
@@ -1045,9 +1042,13 @@ Proof.
 
                destruct tt. destruct tt_limits. simpl.
                rewrite /tab_typing. simpl.
-               apply/andP. split => //=.
-               rewrite /tab_size. simpl. 
-               by rewrite repeat_length.
+               apply/andP. split => /=.
+               - rewrite /tab_size. simpl. 
+                 rewrite repeat_length.
+                 apply/N.leb_spec0.
+                 by rewrite nat_bin N2Nat.id; lias.
+               - destruct lim_max => //.
+                 by apply/N.leb_spec0; lias.
              }
     -- (* memi_agree *)
       rewrite <- Forall2_all2 => /=.
@@ -1090,7 +1091,7 @@ Proof.
 
            destruct mt. 
            rewrite /mem_typing. simpl.
-           apply/andP. split => //=.
+           apply/andP. split => //=; last by destruct lim_max => //; apply/N.leb_spec0; lias.
            rewrite /mem_size /operations.mem_length /memory_list.mem_length. simpl.
            destruct lim_min => //.
            rewrite /page_size. simpl.

theories/instantiation_spec.v

@@ -275,8 +275,8 @@ Definition module_func_typing (c : t_context) (m : module_func) (tf : function_t
     tc_global := c.(tc_global);
     tc_table := c.(tc_table);
     tc_memory := c.(tc_memory);
-    tc_local := c.(tc_local) ++ tn ++ t_locs;
-    tc_label := tm :: c.(tc_label);
+    tc_local := tn ++ t_locs;
+    tc_label := [::tm];
     tc_return := Some tm;
   |} in
   typing.be_typing c' b_es (Tf [::] tm).

theories/interpreter_ctx.v

@@ -734,7 +734,7 @@ Proof.
         inversion Hftype as [s' i tvs C f Hit Hfi Hlocs]; subst.
         destruct fc as [fvs fk ff fes]; simpl in *.
         apply inst_t_context_local_empty in Hit; rewrite -> Hit in *; simpl in *.
-        rewrite length_is_size size_map -length_is_size in H3_getlocal; by lias.
+        rewrite cats0 length_is_size size_map -length_is_size in H3_getlocal; by lias.
 
     - (* AI_basic (BI_set_local j) *)
       get_cc ccs.    
@@ -753,7 +753,7 @@ Proof.
           inversion Hftype as [s' i tvs C f Hit Hfi Hlocs]; subst.
           destruct fc as [fvs fk ff fes]; simpl in *.
           apply inst_t_context_local_empty in Hit; rewrite -> Hit in *; simpl in *.
-          rewrite length_is_size size_map -length_is_size in H3_setlocal; by lias.
+          rewrite cats0 length_is_size size_map -length_is_size in H3_setlocal; by lias.
 
     - (* AI_basic (BI_tee_local j) *)
       destruct vs0 as [|v vs0].

theories/interpreter_func.v

@@ -1917,6 +1917,7 @@ Proof.
     last by apply inst_t_context_local_empty in Hitype'.
   replace (tc_label C''') with ([::] : seq (seq value_type)) in Hetype;
     last by apply inst_t_context_label_empty in Hitype'.
+  rewrite cats0 in Hetype.
   by apply Hetype.
 Qed.