Theory Wasm_Checker

section ‹Executable Type Checker›

theory Wasm_Checker imports Wasm_Checker_Types begin

fun convert_cond :: "t ⇒ t ⇒ sx option ⇒ bool" where
  "convert_cond t1 t2 sx = ((t1 ≠ t2) ∧ (sx = None) = ((is_float_t t1 ∧ is_float_t t2)
                                                        ∨ (is_int_t t1 ∧ is_int_t t2 ∧ (t_length t1 < t_length t2))))"

fun same_lab_h :: "nat list ⇒ (t list) list ⇒ t list ⇒ (t list) option" where
  "same_lab_h [] _ ts = Some ts"
| "same_lab_h (i#is) lab_c ts = (if i ≥ length lab_c
                                 then None
                                 else (if lab_c!i = ts
                                       then same_lab_h is lab_c (lab_c!i)
                                       else None))" 

fun same_lab :: "nat list ⇒ (t list) list ⇒ (t list) option" where
  "same_lab [] lab_c = None"
| "same_lab (i#is) lab_c = (if i ≥ length lab_c
                            then None
                            else same_lab_h is lab_c (lab_c!i))"

lemma same_lab_h_conv_list_all:
  assumes "same_lab_h ils ls ts' = Some ts"
  shows "list_all (λi. i < length ls ∧ ls!i = ts) ils ∧ ts' = ts"
  using assms
proof(induction ils)
  case (Cons a ils)
  thus ?case
    apply (simp,safe)
       apply (metis not_less option.distinct(1))+
    done
qed simp

lemma same_lab_conv_list_all:
  assumes "same_lab ils ls = Some ts"
  shows "list_all (λi. i < length ls ∧ ls!i = ts) ils"
  using assms
proof (induction rule: same_lab.induct)
case (2 i "is" lab_c)
  thus ?case
    using same_lab_h_conv_list_all
    by (metis (mono_tags, lifting) list_all_simps(1) not_less option.distinct(1) same_lab.simps(2))
qed simp

lemma list_all_conv_same_lab_h:
  assumes "list_all (λi. i < length ls ∧ ls!i = ts) ils"
  shows "same_lab_h ils ls ts = Some ts"
  using assms
  by (induction ils, simp_all)

lemma list_all_conv_same_lab:
  assumes "list_all (λi. i < length ls ∧ls!i = ts) (is@[i])"
  shows "same_lab (is@[i]) ls = Some ts"                      
  using assms
proof (induction "(is@[i])")
  case (Cons a x)
  thus ?case
    using list_all_conv_same_lab_h[OF Cons(3)]
    by (metis option.distinct(1) same_lab.simps(2) same_lab_h.simps(2))
qed auto
    
fun b_e_type_checker :: "t_context ⇒  b_e list ⇒ tf ⇒ bool"
and check :: "t_context ⇒ b_e list ⇒ checker_type ⇒ checker_type"
and check_single :: "t_context ⇒  b_e ⇒ checker_type ⇒ checker_type" where
  "b_e_type_checker 𝒞 es (tn _> tm) = c_types_agree (check 𝒞 es (Type tn)) tm"
| "check 𝒞 es ts = (case es of
                     [] ⇒ ts
                   | (e#es) ⇒ (case ts of 
                                  Bot ⇒ Bot
                                | _ ⇒ check 𝒞 es (check_single 𝒞 e ts)))"
(*
foldl (λ ts e. (case ts of Bot ⇒ Bot | _ ⇒ check_single 𝒞 e ts)) es



primrec foldl :: "('b ⇒ 'a ⇒ 'b) ⇒ 'b ⇒ 'a list ⇒ 'b" where
foldl_Nil:  "foldl f a [] = a" |
foldl_Cons: "foldl f a (x # xs) = foldl f (f a x) xs"
*)
  (* num ops *)
| "check_single 𝒞 (C v) ts = type_update ts [] (Type [typeof v])"
| "check_single 𝒞 (Unop_i t _) ts = (if is_int_t t
                                       then type_update ts [TSome t] (Type [t])
                                       else Bot)"
| "check_single 𝒞 (Unop_f t _) ts = (if is_float_t t
                                       then type_update ts [TSome t] (Type [t])
                                       else Bot)"
| "check_single 𝒞 (Binop_i t _) ts = (if is_int_t t
                                       then type_update ts [TSome t, TSome t] (Type [t])
                                       else Bot)"
| "check_single 𝒞 (Binop_f t _) ts = (if is_float_t t
                                       then type_update ts [TSome t, TSome t] (Type [t])
                                       else Bot)"
| "check_single 𝒞 (Testop t _) ts = (if is_int_t t
                                       then type_update ts [TSome t] (Type [T_i32])
                                       else Bot)"
| "check_single 𝒞 (Relop_i t _) ts = (if is_int_t t
                                       then type_update ts [TSome t, TSome t] (Type [T_i32])
                                       else Bot)"
| "check_single 𝒞 (Relop_f t _) ts =  (if is_float_t t
                                       then type_update ts [TSome t, TSome t] (Type [T_i32])
                                       else Bot)"
  (* convert *)
| "check_single 𝒞 (Cvtop t1 Convert t2 sx) ts = (if (convert_cond t1 t2 sx)
                                                   then type_update ts [TSome t2] (Type [t1])
                                                   else Bot)"
  (* reinterpret *)
| "check_single 𝒞 (Cvtop t1 Reinterpret t2 sx) ts = (if ((t1 ≠ t2) ∧ t_length t1 = t_length t2 ∧ sx = None)
                                                         then type_update ts [TSome t2] (Type [t1])
                                                         else Bot)"
  (* unreachable, nop, drop, select *)
| "check_single 𝒞 (Unreachable) ts = type_update ts [] (TopType [])"
| "check_single 𝒞 (Nop) ts = ts"
| "check_single 𝒞 (Drop) ts = type_update ts [TAny] (Type [])"
| "check_single 𝒞 (Select) ts = type_update_select ts"
  (* block *)                                 
| "check_single 𝒞 (Block (tn _> tm) es) ts = (if (b_e_type_checker (𝒞⦇label := ([tm] @ (label 𝒞))⦈) es (tn _> tm))
                                                then type_update ts (to_ct_list tn) (Type tm)
                                                else Bot)"
  (* loop *)
| "check_single 𝒞 (Loop (tn _> tm) es) ts = (if (b_e_type_checker (𝒞⦇label := ([tn] @ (label 𝒞))⦈) es (tn _> tm))
                                                then type_update ts (to_ct_list tn) (Type tm)
                                                else Bot)"
  (* if *)
| "check_single 𝒞 (If (tn _> tm) es1 es2) ts = (if (b_e_type_checker (𝒞⦇label := ([tm] @ (label 𝒞))⦈) es1 (tn _> tm)
                                                    ∧ b_e_type_checker (𝒞⦇label := ([tm] @ (label 𝒞))⦈) es2 (tn _> tm))
                                                then type_update ts (to_ct_list (tn@[T_i32])) (Type tm)
                                                else Bot)"
  (* br *)
| "check_single 𝒞 (Br i) ts = (if i < length (label 𝒞)
                                 then type_update ts (to_ct_list ((label 𝒞)!i)) (TopType [])
                                 else Bot)"
  (* br_if *)
| "check_single 𝒞 (Br_if i) ts = (if i < length (label 𝒞)
                                    then type_update ts (to_ct_list ((label 𝒞)!i @ [T_i32])) (Type ((label 𝒞)!i))
                                    else Bot)"
  (* br_table *)
| "check_single 𝒞 (Br_table is i) ts = (case (same_lab (is@[i]) (label 𝒞)) of
                                        None ⇒ Bot
                                      | Some tls ⇒ type_update ts (to_ct_list (tls @ [T_i32])) (TopType []))"
  (* return *)
| "check_single 𝒞 (Return) ts = (case (return 𝒞) of
                                   None ⇒ Bot
                                 | Some tls ⇒ type_update ts (to_ct_list tls) (TopType []))"
  (* call *)
| "check_single 𝒞 (Call i) ts = (if i < length (func_t 𝒞)
                                    then (case ((func_t 𝒞)!i) of
                                            (tn _> tm) ⇒ type_update ts (to_ct_list tn) (Type tm))
                                    else Bot)"
  (* call_indirect *)
| "check_single 𝒞 (Call_indirect i) ts = (if (table 𝒞) ≠ None ∧ i < length (types_t 𝒞)
                                            then (case ((types_t 𝒞)!i) of
                                                    (tn _> tm) ⇒ type_update ts (to_ct_list (tn@[T_i32])) (Type tm))
                                            else Bot)"
  (* get_local *)
| "check_single 𝒞 (Get_local i) ts = (if i < length (local 𝒞)
                                        then type_update ts [] (Type [(local 𝒞)!i])
                                        else Bot)"
  (* set_local *)
| "check_single 𝒞 (Set_local i) ts = (if i < length (local 𝒞)
                                        then type_update ts [TSome ((local 𝒞)!i)] (Type [])
                                        else Bot)"
  (* tee_local *)
| "check_single 𝒞 (Tee_local i) ts = (if i < length (local 𝒞)
                                 then type_update ts [TSome ((local 𝒞)!i)] (Type [(local 𝒞)!i])
                                 else Bot)"
  (* get_global *)
| "check_single 𝒞 (Get_global i) ts = (if i < length (global 𝒞)
                                         then type_update ts [] (Type [tg_t ((global 𝒞)!i)])
                                         else Bot)"
  (* set_global *)
| "check_single 𝒞 (Set_global i) ts = (if i < length (global 𝒞) ∧ is_mut (global 𝒞 ! i)
                                         then type_update ts [TSome (tg_t ((global 𝒞)!i))] (Type [])
                                         else Bot)"
  (* load *)
| "check_single 𝒞 (Load t tp_sx a off) ts = (if (memory 𝒞) ≠ None ∧ load_store_t_bounds a (option_projl tp_sx) t
                                 then type_update ts [TSome T_i32] (Type [t])
                                 else Bot)"
  (* store *)
| "check_single 𝒞 (Store t tp a off) ts = (if (memory 𝒞) ≠ None ∧ load_store_t_bounds a tp t
                                             then type_update ts [TSome T_i32,TSome t] (Type [])
                                             else Bot)"
  (* current_memory *)
| "check_single 𝒞 Current_memory ts = (if (memory 𝒞) ≠ None
                                         then type_update ts [] (Type [T_i32])
                                         else Bot)"
  (* grow_memory *)
| "check_single 𝒞 Grow_memory ts = (if (memory 𝒞) ≠ None
                                      then type_update ts [TSome T_i32] (Type [T_i32])
                                      else Bot)"

end