JSCert: Certified JavaScript

Inductive expr :=
  | expr_this : expr
  | expr_identifier : string -> expr
  | expr_literal : literal -> expr
  | expr_object : list (propname * propbody) -> expr
  | expr_function : option string -> list string -> funcbody -> expr
  | expr_access : expr -> expr -> expr
  | expr_member : expr -> string -> expr
  | expr_new : expr -> list expr -> expr
  | expr_call : expr -> list expr -> expr
  | expr_unary_op : unary_op -> expr -> expr
  | expr_binary_op : expr -> binary_op -> expr -> expr
  | expr_conditional : expr -> expr -> expr -> expr
  | expr_assign : expr -> option binary_op -> expr -> expr

with stat := 
  | stat_expr : expr -> stat
  | stat_label : string -> stat -> stat
  | stat_block : list stat -> stat
  | stat_var_decl : list (string * option expr) -> stat
  | stat_if : expr -> stat -> option stat -> stat
  | stat_do_while : label_set -> stat -> expr -> stat
  | stat_while : label_set -> expr -> stat -> stat
  | stat_with : expr -> stat -> stat
  | stat_throw : expr -> stat
  | stat_return : option expr -> stat
  | stat_break : label -> stat
  | stat_continue : label ->  stat
  | stat_try : stat -> option (string * stat) -> option stat -> stat (* Note: try s1 [catch (x) s2] [finally s3] *)
  | stat_for : label_set -> option expr -> option expr -> option expr -> stat -> stat (* Note: for (e1; e2; e3) stat *)
  | stat_for_var : label_set -> list (string * option expr) -> option expr -> option expr -> stat -> stat (* Note: for (var ...; e2; e3) stat *)
  | stat_for_in : label_set -> expr -> expr -> stat -> stat (* Note: for (e1 in e2) stat *)
  | stat_for_in_var : label_set -> string -> option expr -> expr -> stat -> stat (*  Note: for (var x [= e1] in e2) stat *)
  | stat_debugger : stat
  | stat_switch : label_set -> expr -> switchbody -> stat

with prog :=
  | prog_intro : strictness_flag -> list element -> prog

with element :=
  | element_stat : stat -> element
  | element_func_decl : string -> list string -> funcbody -> element.

Record funcdecl := funcdecl_intro {
   funcdecl_name : string;
   funcdecl_parameters : list string;
   funcdecl_body : funcbody }.

with funcbody :=
  | funcbody_intro : prog -> string -> funcbody

Inductive literal :=
  | literal_null : literal
  | literal_bool : bool -> literal
  | literal_number : number -> literal
  | literal_string : string -> literal.

Inductive value :=
  | value_prim : prim -> value
  | value_object : object_loc -> value.

Inductive prim :=
  | prim_undef : prim
  | prim_null : prim
  | prim_bool : bool -> prim
  | prim_number : number -> prim
  | prim_string : string -> prim.

Inductive type :=
  | type_undef : type
  | type_null : type
  | type_bool : type
  | type_number : type
  | type_string : type
  | type_object : type.

Record object := object_intro {
   object_proto_ : value;
   object_class_ : class_name;
   object_extensible_ : bool;
   object_prim_value_ : option value;
   object_properties_ : object_properties_type;
   object_get_ : builtin_get;
   object_get_own_prop_ : builtin_get_own_prop;
   object_get_prop_ : builtin_get_prop;
   object_put_ : builtin_put;
   object_can_put_ : builtin_can_put;
   object_has_prop_ : builtin_has_prop;
   object_delete_ : builtin_delete;
   object_default_value_ : builtin_default_value;
   object_define_own_prop_ : builtin_define_own_prop;
   object_construct_ : option construct;
   object_call_ : option call ;
   object_has_instance_ : option builtin_has_instance;
   object_scope_ : option lexical_env;
   object_formal_parameters_ : option (list string);
   object_code_ : option funcbody;
   object_target_function_ : option object_loc;
   object_bound_this_ : option value;
   object_bound_args_ : option (list value);
   object_parameter_map_ : option object_loc }.

Definition object_properties_type :=
  Heap.heap prop_name attributes.

Inductive attributes :=
  | attributes_data_of : attributes_data -> attributes
  | attributes_accessor_of : attributes_accessor -> attributes.

Inductive full_descriptor :=
  | full_descriptor_undef : full_descriptor
  | full_descriptor_some : attributes -> full_descriptor.

Record attributes_data := attributes_data_intro {
   attributes_data_value : value;
   attributes_data_writable : bool;
   attributes_data_enumerable : bool;
   attributes_data_configurable : bool }.

Record attributes_accessor := attributes_accessor_intro {
   attributes_accessor_get : value;
   attributes_accessor_set : value;
   attributes_accessor_enumerable : bool;
   attributes_accessor_configurable : bool }.

Record descriptor := descriptor_intro {
   descriptor_value : option value;
   descriptor_writable : option bool;
   descriptor_get : option value;
   descriptor_set : option value;
   descriptor_enumerable : option bool;
   descriptor_configurable : option bool }.

Record execution_ctx := execution_ctx_intro {
   execution_ctx_lexical_env : lexical_env;
   execution_ctx_variable_env : lexical_env;
   execution_ctx_this_binding : value;
   execution_ctx_strict : strictness_flag }.

Definition lexical_env := list env_loc.

Inductive env_record :=
  | env_record_decl : decl_env_record -> env_record
  | env_record_object : object_loc -> provide_this_flag -> env_record.

Definition lexical_env := list env_loc.

Inductive env_record :=
  | env_record_decl : decl_env_record -> env_record
  | env_record_object : object_loc -> provide_this_flag -> env_record.

Inductive mutability :=
  | mutability_uninitialized_immutable
  | mutability_immutable
  | mutability_nondeletable
  | mutability_deletable.

Record state := state_intro {
   state_object_heap : Heap.heap object_loc object;
   state_env_record_heap : Heap.heap env_loc env_record;
   state_fresh_locations : stream nat;
   state_event_list : list event }.

Record ref := ref_intro {
  ref_base : ref_base_type;
  ref_name : prop_name;
  ref_strict : bool }.

Inductive ref_base_type :=
  | ref_base_type_value : value -> ref_base_type
  | ref_base_type_env_loc : env_loc -> ref_base_type.

Inductive res := res_intro {
  res_type : restype;
  res_value : resvalue;
  res_label : label }.

Inductive restype :=
  | restype_normal
  | restype_break
  | restype_continue
  | restype_return
  | restype_throw.

Inductive resvalue :=
  | resvalue_empty : resvalue
  | resvalue_value : value -> resvalue
  | resvalue_ref : ref -> resvalue.

Inductive label :=
   | label_empty : label
   | label_string : string -> label.

Definition res_empty := res_intro restype_normal resvalue_empty label_empty.

Definition res_break labo := res_intro restype_break resvalue_empty labo.

Definition res_continue labo := res_intro restype_continue resvalue_empty labo.

Definition res_return v := res_intro restype_return v label_empty.

Definition res_throw v := res_intro restype_throw v label_empty.

Coercion res_normal rv := res_intro restype_normal rv label_empty.

Coercion res_val (v : value) := res_intro restype_normal v label_empty.

Coercion res_ref (r : ref) := res_intro restype_normal r label_empty.

Definition abrupt_res R :=
  res_type R <> restype_normal.

Inductive out :=
  | out_div : out
  | out_ter : state -> res -> out.

Inductive specret (T : Type) :=
  | specret_val : state -> T -> specret T
  | specret_out : out -> specret T.

Definition object_binds S l O :=
  Heap.binds (state_object_heap S) l O.

Definition object_binds_property S l x A :=
  exists O, object_binds S l O /\ Heap.binds (object_properties_ O) x A.

Definition object_set_property S l x A S' :=
  object_heap_map_properties S l (fun P => Heap.write P x A) S'.

Definition object_heap_map_properties S l F S' :=
  exists O, object_binds S l O
         /\ S' = object_write S l (object_map_properties O F).

Definition object_map_properties O F :=
  object_with_properties O (F (object_properties_ O)).

Fixpoint stat_vardecl (t : stat) : list string :=
  match t with
  | stat_expr _ => nil
  | stat_label _ s => stat_vardecl s
  | stat_block ts => LibList.concat (List.map stat_vardecl ts) 
  | stat_var_decl nes => LibList.map fst nes
  | stat_if e s1 s2o => (stat_vardecl s1) ++
                        (LibOption.unsome_default 
                           nil
                           (LibOption.map stat_vardecl s2o))
  | stat_do_while _ s _ => stat_vardecl s
  | stat_while _ _ s => stat_vardecl s
  | stat_with _ s => stat_vardecl s
  | stat_throw _ => nil
  | stat_return _ => nil
  | stat_break _ => nil
  | stat_continue _ => nil
  | stat_try s sco sfo => (stat_vardecl s) ++
                          (LibOption.unsome_default 
                             nil
                             (LibOption.map 
                                (fun sc => stat_vardecl (snd sc)) sco)) ++
                          (LibOption.unsome_default 
                             nil
                             (LibOption.map stat_vardecl sfo))
  | stat_for _ _ _ _ s => stat_vardecl s
  | stat_for_var _ nes _ _ s => LibList.map fst nes ++ stat_vardecl s
  | stat_for_in _ _ _ s => stat_vardecl s
  | stat_for_in_var _ str _ _ s => str :: stat_vardecl s
  | stat_debugger => nil
  | stat_switch _ _ sb => switchbody_vardecl sb
  end

with switchbody_vardecl (sb : switchbody) : list string :=
  match sb with
  | switchbody_nodefault scl => LibList.concat (List.map switchclause_vardecl scl)
  | switchbody_withdefault scl1 sl scl2 =>
    (LibList.concat (List.map switchclause_vardecl scl1)) ++
    (LibList.concat (List.map stat_vardecl sl)) ++
    (LibList.concat (List.map switchclause_vardecl scl2))
  end

with switchclause_vardecl (sc : switchclause) : list string :=
  match sc with
  | switchclause_intro _ sl => LibList.concat (List.map stat_vardecl sl)
  end.

Definition element_vardecl (el : element) : list string :=
  match el with
  | element_stat t => stat_vardecl t
  | element_func_decl name args bd => nil
  end.

Definition prog_vardecl (p : prog) : list string :=
  LibList.concat (LibList.map element_vardecl (prog_elements p)).

Definition prog_funcdecl (p : prog) : list funcdecl :=
  LibList.concat (LibList.map element_funcdecl (prog_elements p)).

Definition element_funcdecl (el : element) : list funcdecl :=
  match el with
  | element_stat _ => nil
  | element_func_decl name args bd =>
      funcdecl_intro name args bd :: nil
  end.

Definition convert_value_to_boolean v :=
  match v with
  | value_prim p => convert_prim_to_boolean p
  | value_object _ => true
  end.

Definition convert_prim_to_boolean w :=
  match w with
  | prim_undef => false
  | prim_null => false
  | prim_bool b => b
  | prim_number n => convert_number_to_bool n
  | prim_string s => convert_string_to_bool s
  end.

Definition convert_number_to_bool n :=
  ifb (n = JsNumber.zero \/ n = JsNumber.neg_zero \/ n = JsNumber.nan)
    then false
    else true.

Definition convert_prim_to_number w :=
  match w with
  | prim_undef => JsNumber.nan
  | prim_null => JsNumber.zero
  | prim_bool b => if b then JsNumber.one else JsNumber.zero
  | prim_number n => n
  | prim_string s => JsNumber.from_string s
  end.

Definition inequality_test_primitive w1 w2 : prim :=
  match w1, w2 with
  | prim_string s1, prim_string s2 => inequality_test_string s1 s2
  | _, _ => inequality_test_number (convert_prim_to_number w1) (convert_prim_to_number w2)
  end.

Fixpoint inequality_test_string s1 s2 : bool :=
  match s1, s2 with
  | _, EmptyString => false
  | EmptyString, String _ _ => true
  | String c1 s1', String c2 s2' =>
     ifb c1 = c2
       then inequality_test_string s1' s2'
       else decide (int_of_char c1 < int_of_char c2)
  end.

Definition inequality_test_number n1 n2 : prim :=
  ifb n1 = JsNumber.nan \/ n2 = JsNumber.nan then prim_undef
  else ifb n1 = n2 then false
  else ifb n1 = JsNumber.zero /\ n2 = JsNumber.neg_zero then false
  else ifb n1 = JsNumber.neg_zero /\ n2 = JsNumber.zero then false
  else ifb n1 = JsNumber.infinity then false
  else ifb n2 = JsNumber.infinity then true
  else ifb n2 = JsNumber.neg_infinity then false
  else ifb n1 = JsNumber.neg_infinity then true
  else JsNumber.lt_bool n1 n2.

Axiom parse : string -> option prog -> Prop.
Axiom parse_exists : forall s, exists oprog, parse s oprog.
Axiom parse_pickable : forall s, Pickable (parse s).

Definition object_heap_initial_function_objects_1 (h : Heap.heap object_loc object) :=
  (* ThrowTypeError Function object *)
  let h := Heap.write h prealloc_throw_type_error throw_type_error_object in

  (* Function objects of Global object *)
  let h := Heap.write h prealloc_global_eval global_eval_function_object in
  let h := Heap.write h prealloc_global_is_nan global_is_nan_function_object in
  let h := Heap.write h prealloc_global_is_finite global_is_finite_function_object in h.

Definition object_heap_initial_function_objects_1 (h : Heap.heap object_loc object) :=
  (* ThrowTypeError Function object *)
  let h := Heap.write h prealloc_throw_type_error throw_type_error_object in

  (* Function objects of Global object *)
  let h := Heap.write h prealloc_global_eval global_eval_function_object in
  let h := Heap.write h prealloc_global_is_nan global_is_nan_function_object in
  let h := Heap.write h prealloc_global_is_finite global_is_finite_function_object in h.

Definition object_heap_initial_function_objects_3 (h : Heap.heap object_loc object) :=
  let h := object_heap_initial_function_objects_2 h in 
  (* Function objects of Object.prototype *)
  let h := Heap.write h prealloc_object_proto_to_string object_proto_to_string_function_object in
  let h := Heap.write h prealloc_object_proto_value_of object_proto_value_of_function_object in
  let h := Heap.write h prealloc_object_proto_has_own_prop object_proto_has_own_prop_function_object in
  let h := Heap.write h prealloc_object_proto_is_prototype_of object_proto_is_prototype_of_function_object in
  let h := Heap.write h prealloc_object_proto_prop_is_enumerable object_proto_prop_is_enumerable_function_object in

  (* Function objects of Array.prototype *)
  let h := Heap.write h prealloc_array_proto_pop array_proto_pop_function_object in
  let h := Heap.write h prealloc_array_proto_push array_proto_push_function_object in

  (* Function objects of String.prototype *)
  let h := Heap.write h prealloc_string_proto_to_string string_proto_to_string_function_object in
  let h := Heap.write h prealloc_string_proto_value_of string_proto_value_of_function_object in

  (* Function objects of Boolean.prototype *)
  let h := Heap.write h prealloc_bool_proto_to_string bool_proto_to_string_function_object in
  let h := Heap.write h prealloc_bool_proto_value_of bool_proto_value_of_function_object in h.

Definition object_heap_initial_function_objects_2 (h : Heap.heap object_loc object) :=
  let h := object_heap_initial_function_objects_1 h in 
  (* Function objects of Object *)
  let h := Heap.write h prealloc_object_get_proto_of object_get_proto_of_function_object in
  let h := Heap.write h prealloc_object_get_own_prop_descriptor object_get_own_prop_descriptor_function_object in
  let h := Heap.write h prealloc_object_get_own_prop_name object_get_own_prop_name_function_object in
  let h := Heap.write h prealloc_object_create object_create_function_object in
  let h := Heap.write h prealloc_object_define_prop object_define_prop_function_object in
  let h := Heap.write h prealloc_object_define_props object_define_props_function_object in
  let h := Heap.write h prealloc_object_seal object_seal_function_object in
  let h := Heap.write h prealloc_object_freeze object_freeze_function_object in
  let h := Heap.write h prealloc_object_prevent_extensions object_prevent_extensions_function_object in
  let h := Heap.write h prealloc_object_is_sealed object_is_sealed_function_object in
  let h := Heap.write h prealloc_object_is_frozen object_is_frozen_function_object in
  let h := Heap.write h prealloc_object_is_extensible object_is_extensible_function_object in h.

Definition object_heap_initial_function_objects_1 (h : Heap.heap object_loc object) :=
  (* ThrowTypeError Function object *)
  let h := Heap.write h prealloc_throw_type_error throw_type_error_object in

  (* Function objects of Global object *)
  let h := Heap.write h prealloc_global_eval global_eval_function_object in
  let h := Heap.write h prealloc_global_is_nan global_is_nan_function_object in
  let h := Heap.write h prealloc_global_is_finite global_is_finite_function_object in h.

Definition object_prealloc_global_properties :=
  let P := Heap.empty in
  let P := write_constant P "NaN" JsNumber.nan in
  let P := write_constant P "Infinity" JsNumber.infinity in
  let P := write_constant P "undefined" undef in
  let P := write_native P "eval" prealloc_global_eval in
  let P := write_native P "isNaN" prealloc_global_is_nan in
  let P := write_native P "isFinite" prealloc_global_is_finite in
  let P := write_native P "Object" prealloc_object in
  let P := write_native P "Function" prealloc_function in
  let P := write_native P "Array" prealloc_array in
  let P := write_native P "String" prealloc_string in
  let P := write_native P "Boolean" prealloc_bool in
  let P := write_native P "Number" prealloc_number in
  let P := write_native P "Error" prealloc_error in
  let P := write_native P "EvalError" native_error_eval in
  let P := write_native P "RangeError" native_error_range in
  let P := write_native P "ReferenceError" native_error_ref in
  let P := write_native P "SyntaxError" native_error_syntax in
  let P := write_native P "TypeError" native_error_type in
  P.

Parameter object_prealloc_global_proto : value.
Parameter object_prealloc_global_class : string.

Definition object_prealloc_global_properties :=
  let P := Heap.empty in
  let P := write_constant P "NaN" JsNumber.nan in
  let P := write_constant P "Infinity" JsNumber.infinity in
  let P := write_constant P "undefined" undef in
  let P := write_native P "eval" prealloc_global_eval in
  let P := write_native P "isNaN" prealloc_global_is_nan in
  let P := write_native P "isFinite" prealloc_global_is_finite in
  let P := write_native P "Object" prealloc_object in
  let P := write_native P "Function" prealloc_function in
  let P := write_native P "Array" prealloc_array in
  let P := write_native P "String" prealloc_string in
  let P := write_native P "Boolean" prealloc_bool in
  let P := write_native P "Number" prealloc_number in
  let P := write_native P "Error" prealloc_error in
  let P := write_native P "EvalError" native_error_eval in
  let P := write_native P "RangeError" native_error_range in
  let P := write_native P "ReferenceError" native_error_ref in
  let P := write_native P "SyntaxError" native_error_syntax in
  let P := write_native P "TypeError" native_error_type in
  P.

Definition global_is_nan_function_object := 
  object_create_prealloc_call prealloc_global_is_nan 1 Heap.empty.

Inductive ext_expr :=

  (** Extended expressions include expressions *)

  | expr_basic : expr -> ext_expr

  (** Extended expressions associated with primitive expressions *)

  | expr_identifier_1 : specret ref -> ext_expr

  | expr_object_0 : out -> propdefs -> ext_expr
  | expr_object_1 : object_loc -> propdefs -> ext_expr
  | expr_object_2 : object_loc -> string -> propbody -> propdefs -> ext_expr 
  | expr_object_3_val : object_loc -> string -> specret value -> propdefs -> ext_expr
  | expr_object_3_get : object_loc -> string -> out -> propdefs -> ext_expr
  | expr_object_3_set : object_loc -> string -> out -> propdefs -> ext_expr
  | expr_object_4 : object_loc -> string -> attributes -> propdefs -> ext_expr
  | expr_object_5 : object_loc -> propdefs -> out -> ext_expr

  | expr_function_1 : string -> list string -> funcbody -> env_loc -> lexical_env -> out -> ext_expr
  | expr_function_2 : string -> env_loc -> out -> ext_expr
  | expr_function_3 : object_loc -> out -> ext_expr

  | expr_access_1 : specret value -> expr -> ext_expr (* The left expression has been executed *)
  | expr_access_2 : value -> specret value -> ext_expr (* The right expression is executed. *)
  | expr_access_3 : value -> out -> value -> ext_expr
  | expr_access_4 : value -> out -> ext_expr

  | expr_new_1 : (specret value) -> list expr -> ext_expr (* The arguments too. *)
  | expr_new_2 : value -> (specret (list value)) -> ext_expr (* The call has been executed. *)

  | expr_call_1 : out -> bool -> list expr -> ext_expr
  | expr_call_2 : res -> bool -> list expr -> (specret value) -> ext_expr (* The function has been evaluated. *)
  | expr_call_3 : res -> value -> bool -> (specret (list value)) -> ext_expr (* The arguments have been executed. *)
  | expr_call_4 : res -> object_loc -> bool -> list value -> ext_expr
  | expr_call_5

with ext_stat :=

  (** Extended expressions include statements *)

  | stat_basic : stat -> ext_stat

  (** Extended statements associated with primitive statements *)
  | stat_expr_1: (specret value) -> ext_stat

  | stat_block_1 : out -> stat -> ext_stat
  | stat_block_2 : resvalue -> out -> ext_stat

  | stat_label_1 : label -> out -> ext_stat

  | stat_var_decl_1 : out -> list (string * option expr) -> ext_stat
  | stat_var_decl_item : (string * option expr) -> ext_stat
  | stat_var_decl_item_1 : string -> specret ref -> expr -> ext_stat
  | stat_var_decl_item_2 : string -> ref -> (specret value) -> ext_stat
  | stat_var_decl_item_3 : string -> out -> ext_stat

  | stat_if_1 : specret value -> stat -> option stat -> ext_stat

  | stat_while_1 : label_set -> expr -> stat -> resvalue -> ext_stat
  | stat_while_2 : label_set -> expr -> stat -> resvalue -> specret value -> ext_stat
  | stat_while_3 : label_set -> expr -> stat -> resvalue -> out -> ext_stat
  | stat_while_4 : label_set -> expr -> stat -> resvalue -> res -> ext_stat
  | stat_while_5 : label_set -> expr -> stat -> resvalue -> res -> ext_stat
  | stat_while_6

with ext_prog :=

  | prog_basic : prog -> ext_prog
  | javascript_1 : out -> prog -> ext_prog
  | prog_1 : out -> element -> ext_prog
  | prog_2

with ext_spec :=
  | spec_to_int32 : value -> ext_spec
  | spec_to_int32_1 : out -> ext_spec
  | spec_to_uint32 : value -> ext_spec
  | spec_to_uint32_1 : out -> ext_spec

  | spec_expr_get_value_conv : (value -> ext_expr) -> expr -> ext_spec
  | spec_expr_get_value_conv_1 : (value -> ext_expr) -> (specret value) -> ext_spec
  | spec_expr_get_value_conv_2 : out -> ext_spec

  | spec_convert_twice : ext_expr -> ext_expr -> ext_spec
  | spec_convert_twice_1 : out -> ext_expr -> ext_spec
  | spec_convert_twice_2 : value -> out -> ext_spec

  (** Extended expressions for lists of expressions *)
  | spec_list_expr : list expr -> ext_spec
  | spec_list_expr_1 : list value -> list expr -> ext_spec
  | spec_list_expr_2 : list value -> (specret value) -> list expr -> ext_spec 

  | spec_to_descriptor : value -> ext_spec
  | spec_to_descriptor_1a : object_loc -> descriptor -> ext_spec
  | spec_to_descriptor_1b : out -> object_loc -> descriptor -> ext_spec
  | spec_to_descriptor_1c : out -> object_loc -> descriptor -> ext_spec
  | spec_to_descriptor_2a : object_loc -> descriptor -> ext_spec                            
  | spec_to_descriptor_2b : out -> object_loc -> descriptor -> ext_spec
  | spec_to_descriptor_2c : out -> object_loc -> descriptor -> ext_spec
  | spec_to_descriptor_3a : object_loc -> descriptor -> ext_spec                            
  | spec_to_descriptor_3b : out -> object_loc -> descriptor -> ext_spec
  | spec_to_descriptor_3c : out -> object_loc -> descriptor -> ext_spec
  | spec_to_descriptor_4a : object_loc -> descriptor -> ext_spec                            
  | spec_to_descriptor_4b : out -> object_loc -> descriptor -> ext_spec
  | spec_to_descriptor_4c : out -> object_loc -> descriptor -> ext_spec
  | spec_to_descriptor_5a : object_loc -> descriptor -> ext_spec                            
  | spec_to_descriptor_5b : out -> object_loc -> descriptor -> ext_spec
  | spec_to_descriptor_5c : out -> object_loc -> descriptor -> ext_spec
  | spec_to_descriptor_6a : object_loc -> descriptor -> ext_spec                            
  | spec_to_descriptor_6b : out -> object_loc -> descriptor -> ext_spec
  | spec_to_descriptor_6c : out -> object_loc -> descriptor -> ext_spec
  | spec_to_descriptor_7 : object_loc -> descriptor -> ext_spec    

  | spec_object_get_own_prop : object_loc -> prop_name -> ext_spec
  | spec_object_get_own_prop_1 : builtin_get_own_prop -> object_loc -> prop_name -> ext_spec
  | spec_object_get_own_prop_2

Inductive red_javascript : prog -> out -> Prop :=

with red_prog : state -> execution_ctx -> ext_prog -> out -> Prop :=

with red_stat : state -> execution_ctx -> ext_stat -> out -> Prop :=

with red_expr : state -> execution_ctx -> ext_expr -> out -> Prop :=

with red_spec : forall {T}, state -> execution_ctx -> ext_spec -> specret T -> Prop :=

Inductive red_javascript : prog -> out -> Prop :=

  | red_javascript_intro : forall S C p p' o o1,
      S = state_initial ->
      p' = add_infos_prog strictness_false p ->
      C = execution_ctx_initial (prog_intro_strictness p') -> 
      red_expr S C (spec_binding_inst codetype_global None p' nil) o1 ->
      red_prog S C (javascript_1 o1 p') o ->
      red_javascript p o

| red_expr_access : forall S C e1 e2 y1 o,
    red_spec S C (spec_expr_get_value e1) y1 ->
    red_expr S C (expr_access_1 y1 e2) o ->
    red_expr S C (expr_access e1 e2) o

| red_expr_access_1 : forall S0 S C v1 e2 y1 o,
    red_spec S C (spec_expr_get_value e2) y1 ->
    red_expr S C (expr_access_2 v1 y1) o ->
    red_expr S0 C (expr_access_1 (ret S v1) e2) o

| red_expr_access_2 : forall S0 S C v1 v2 o1 o,
    red_expr S C (spec_check_object_coercible v1) o1 ->
    red_expr S C (expr_access_3 v1 o1 v2) o ->
    red_expr S0 C (expr_access_2 v1 (ret S v2)) o

| red_expr_access_3 : forall S0 S C v1 v2 o1 o,
    red_expr S C (spec_to_string v2) o1 ->
    red_expr S C (expr_access_4 v1 o1) o ->
    red_expr S0 C (expr_access_3 v1 (out_void S) v2) o

| red_expr_access_4 : forall S0 S C v1 x r,
   r = ref_create_value v1 x (execution_ctx_strict C) ->
   red_expr S0 C (expr_access_4 v1 (out_ter S x)) (out_ter S r)

| red_stat_if : forall S C e1 t2 t3opt y1 o,
    red_spec S C (spec_expr_get_value_conv spec_to_boolean e1) y1 ->
    red_stat S C (stat_if_1 y1 t2 t3opt) o ->
    red_stat S C (stat_if e1 t2 t3opt) o

| red_stat_if_1_true : forall S0 S C t2 t3opt o,
    red_stat S C t2 o ->
    red_stat S0 C (stat_if_1 (vret S true) t2 t3opt) o

| red_stat_if_1_false : forall S0 S C t2 t3 o,
    red_stat S C t3 o ->
    red_stat S0 C (stat_if_1 (vret S false) t2 (Some t3)) o

| red_stat_if_1_false_implicit : forall S0 S C t2,
    red_stat S0 C (stat_if_1 (vret S false) t2 None) (out_ter S resvalue_empty)

| red_stat_while : forall S C labs e1 t2 o,
    red_stat S C (stat_while_1 labs e1 t2 resvalue_empty) o ->
    red_stat S C (stat_while labs e1 t2) o

(* Steps 2a and 2b: red_while_2a_2b in POPL14 *)
| red_stat_while_1 : forall S C labs e1 t2 rv y1 o,
    red_spec S C (spec_expr_get_value_conv spec_to_boolean e1) y1 ->
    red_stat S C (stat_while_2 labs e1 t2 rv y1) o ->
    red_stat S C (stat_while_1 labs e1 t2 rv) o

(* Step 2b False: red_while_2b'_false in POPL14 *)
| red_stat_while_2_false : forall S0 S C labs e1 t2 rv,
    red_stat S0 C (stat_while_2 labs e1 t2 rv (vret S false)) (out_ter S rv)

(* Step 2b True and 2c: red_while_2b'_true_2c in POPL14 *)
| red_stat_while_2_true : forall S0 S C labs e1 t2 rv o1 o,
    red_stat S C t2 o1 ->
    red_stat S C (stat_while_3 labs e1 t2 rv o1) o ->
    red_stat S0 C (stat_while_2 labs e1 t2 rv (vret S true)) o

(* Step 2d: red_while_2d in POPL14 *)
| red_stat_while_3 : forall rv S0 S C labs e1 t2 rv' R o,
    rv' = (If res_value R <> resvalue_empty then res_value R else rv) ->
    red_stat S C (stat_while_4 labs e1 t2 rv' R) o ->
    red_stat S0 C (stat_while_3 labs e1 t2 rv (out_ter S R)) o

(* Step 2e False: red_while_2e_false in POPL14 *)
| red_stat_while_4_continue : forall S C labs e1 t2 rv R o,
    res_type R = restype_continue /\ res_label_in R labs ->
    red_stat S C (stat_while_1 labs e1 t2 rv) o ->
    red_stat S C (stat_while_4 labs e1 t2 rv R) o

(* Step 2e True: red_while_2e_true in POPL14 *)
| red_stat_while_4_not_continue : forall S C labs e1 t2 rv R o,
    ~ (res_type R = restype_continue /\ res_label_in R labs) ->
    red_stat S C (stat_while_5 labs e1 t2 rv R) o ->
    red_stat S C (stat_while_4 labs e1 t2 rv R) o

(* Step 2e i True: red_while_2e_i_true in POPL14 *)
| red_stat_while_5_break : forall S C labs e1 t2 rv R,
    res_type R = restype_break /\ res_label_in R labs ->
    red_stat S C (stat_while_5 labs e1 t2 rv R) (out_ter S rv)

(* Step 2e i False: red_while_2e_i_false in POPL14 *)
| red_stat_while_5_not_break : forall S C labs e1 t2 rv R o,
    ~ (res_type R = restype_break /\ res_label_in R labs) ->
    red_stat S C (stat_while_6 labs e1 t2 rv R) o ->
    red_stat S C (stat_while_5 labs e1 t2 rv R) o

(* Step 2e ii True: red_while_2e_ii_true in POPL14 *)
| red_stat_while_6_abort : forall S C labs e1 t2 rv R,
    res_type R <> restype_normal ->
    red_stat S C (stat_while_6 labs e1 t2 rv R) (out_ter S R)

(* Step 2e ii False: red_while_2e_ii_false in POPL14 *)
| red_stat_while_6_normal : forall S C labs e1 t2 rv R o,
    res_type R = restype_normal ->
    red_stat S C (stat_while_1 labs e1 t2 rv) o ->
    red_stat S C (stat_while_6 labs e1 t2 rv R) o

| red_spec_call_object_proto_to_string : forall S C vthis args o, 
    red_expr S C (spec_call_object_proto_to_string_1 vthis) o ->
    red_expr S C (spec_call_prealloc prealloc_object_proto_to_string vthis args) o

| red_spec_call_object_proto_to_string_1_undef : forall S C, 
    red_expr S C (spec_call_object_proto_to_string_1 undef) (out_ter S "[object Undefined]"%string)

| red_spec_call_object_proto_to_string_1_null : forall S C, 
    red_expr S C (spec_call_object_proto_to_string_1 null) (out_ter S "[object Null]"%string)

| red_spec_call_object_proto_to_string_1_other : forall S C v o o1, 
    ~ (v = null \/ v = undef) ->
    red_expr S C (spec_to_object v) o1 ->
    red_expr S C (spec_call_object_proto_to_string_2 o1) o ->
    red_expr S C (spec_call_object_proto_to_string_1 v) o

| red_spec_call_object_proto_to_string_2 : forall S0 S C l s sclass,
    object_class S l sclass ->
    s = "[object " ++ sclass ++ "]" ->
    red_expr S0 C (spec_call_object_proto_to_string_2 (out_ter S l)) (out_ter S s)

Inductive search_proto_chain : state -> object_loc -> prop_name -> option object_loc -> Prop :=
  | search_proto_chain_found : forall S l x,
                                 object_has_property S l x ->
                                 search_proto_chain S l x (Some l)
  | search_proto_chain_not_found : forall S l x,
                                     not (object_has_property S l x) ->
                                     object_proto S l prim_null ->
                                     search_proto_chain S l x None
  | search_proto_chain_inductive : forall S l x v l' res,
                                     not (object_has_property S l x) ->
                                     object_proto S l (value_object l') ->
                                     search_proto_chain S l' x res ->
                                     search_proto_chain S l x res.

Inductive arguments_from : list value -> list value -> Prop :=
 | arguments_from_nil : forall Vs,
      arguments_from Vs nil
 | arguments_from_undef : forall Vs: list value,
      arguments_from nil Vs ->
      arguments_from nil (undef::Vs)
 | arguments_from_cons : forall Vs1 Vs2 v,
      arguments_from Vs1 Vs2 ->
      arguments_from (v::Vs1) (v::Vs2).

| red_stat_abort : forall S C extt o, (* called red_stat_exception in POPL14 *)
    out_of_ext_stat extt = Some o ->
    abort o ->
    ~ abort_intercepted_stat extt ->
    red_stat S C extt o

Inductive abort : out -> Prop :=
  | abort_div :
      abort out_div
  | abort_not_normal : forall S R,
      ~ res_is_normal R ->
      abort (out_ter S R).

Definition out_of_ext_stat (p : ext_stat) : option out :=
  match p with
  | stat_expr_1 (specret_out o) => Some o
  | stat_expr_1 (specret_val _ _) => None
  | stat_basic _ => None

  | stat_block_1 o _ => Some o
  | stat_block_2 _ o => Some o

  | stat_label_1 _ o => Some o

  | stat_var_decl_1 o _ => Some o
  | stat_var_decl_item _ => None
  | stat_var_decl_item_1 _ y _ => out_of_specret y
  | stat_var_decl_item_2 _ _ y => out_of_specret y
  | stat_var_decl_item_3 _ o => Some o

  | stat_if_1 y _ _ => out_of_specret y

  | stat_while_1 _ _ _ _ => None
  | stat_while_2 _ _ _ _ y => out_of_specret y
  | stat_while_3 _ _ _ _ o => Some o
  | stat_while_4 _ _ _ _ _ => None
  | stat_while_5 _ _ _ _ _ => None
  | stat_while_6 _ _ _ _ _ => None

Inductive abort_intercepted_stat : ext_stat -> Prop :=

  | abort_intercepted_stat_block_2 : forall S R rv,
      abort_intercepted_stat (stat_block_2 rv (out_ter S R))
  | abort_intercepted_stat_label_1 : forall lab rv S R,
      R = res_intro restype_break rv lab ->
      abort_intercepted_stat (stat_label_1 lab (out_ter S R))
  | abort_intercepted_do_while_2 : forall labs e1 t2 rv S R,
      res_label_in R labs ->
      (res_type R = restype_continue \/ res_type R = restype_break) ->
      abort_intercepted_stat (stat_do_while_2 labs t2 e1 rv (out_ter S R))
  | abort_intercepted_while_3 : forall labs e1 t2 rv S R,
      res_label_in R labs ->
      (res_type R = restype_continue \/ res_type R = restype_break) ->
      abort_intercepted_stat (stat_while_3 labs e1 t2 rv (out_ter S R))
  | abort_intercepted_stat_try_1 : forall S R cb fo,
      res_type R = restype_throw ->
      abort_intercepted_stat (stat_try_1 (out_ter S R) (Some cb) fo)
  | abort_intercepted_stat_try_3 : forall S R fo,
      abort_intercepted_stat (stat_try_3 (out_ter S R) fo)

Inductive resultof T :=
  | result_some : T -> resultof T
  | result_not_yet_implemented
  | result_impossible
  | result_bottom : state -> resultof T.

Definition specres T := resultof (specret T).

Record runs_type : Type := runs_type_intro {
    runs_type_expr : state -> execution_ctx -> expr -> result;
    runs_type_stat : state -> execution_ctx -> stat -> result;
    runs_type_prog : state -> execution_ctx -> prog -> result;
    runs_type_call : state -> execution_ctx -> object_loc -> value -> list value -> result;
    runs_type_function_has_instance : state -> object_loc -> value -> result;
    runs_type_stat_while : state -> execution_ctx -> resvalue -> label_set -> expr -> stat -> result;
    runs_type_stat_do_while : state -> execution_ctx -> resvalue -> label_set -> expr -> stat -> result;
    runs_type_stat_for_loop : state -> execution_ctx -> label_set -> resvalue -> option expr -> option expr -> stat -> result;
    runs_type_object_delete : state -> execution_ctx -> object_loc -> prop_name -> bool -> result;
    runs_type_object_get_own_prop : state -> execution_ctx -> object_loc -> prop_name -> specres full_descriptor;
    runs_type_object_get_prop : state -> execution_ctx -> object_loc -> prop_name -> specres full_descriptor;
    runs_type_object_get : state -> execution_ctx -> object_loc -> prop_name -> result;
    runs_type_object_proto_is_prototype_of : state -> object_loc -> object_loc -> result;
    runs_type_object_put : state -> execution_ctx -> object_loc -> prop_name -> value -> strictness_flag -> result;
    runs_type_equal : state -> execution_ctx -> value -> value -> result;
    runs_type_to_integer : state -> execution_ctx -> value -> result;
    runs_type_to_string : state -> execution_ctx -> value -> result
  }.

Definition run_javascript runs p : result :=
  let S := state_initial in
  let p' := add_infos_prog strictness_false p in
  let C := execution_ctx_initial (prog_intro_strictness p') in
  if_void (execution_ctx_binding_inst runs S C codetype_global None p' nil) (fun S' =>
    runs_type_prog runs S' C p').

Definition run_expr_access runs S C e1 e2 : result :=
  if_spec (run_expr_get_value runs S C e1) (fun S1 v1 =>
    if_spec (run_expr_get_value runs S1 C e2) (fun S2 v2 =>
      ifb v1 = prim_undef \/ v1 = prim_null then
        run_error S2 native_error_type
      else
        if_string (to_string runs S2 C v2) (fun S3 x =>
          res_ter S3 (ref_create_value v1 x (execution_ctx_strict C))))).

Definition run_stat_if runs S C e1 t2 to : result :=
  if_spec (run_expr_get_value runs S C e1) (fun S1 v1 =>
    Let b := convert_value_to_boolean v1 in
    if b then
      runs_type_stat runs S1 C t2
    else
      match to with
      | Some t3 =>
        runs_type_stat runs S1 C t3
      | None =>
        out_ter S1 resvalue_empty
      end).

Definition run_stat_while runs S C rv labs e1 t2 : result :=
  if_spec (run_expr_get_value runs S C e1) (fun S1 v1 =>
    Let b := convert_value_to_boolean v1 in
    if b then
      if_ter (runs_type_stat runs S1 C t2) (fun S2 R =>
        Let rv' := ifb res_value R <> resvalue_empty then res_value R else rv in
        Let loop := fun _ => runs_type_stat_while runs S2 C rv' labs e1 t2 in
        ifb res_type R <> restype_continue
             \/ ~ res_label_in R labs then (
           ifb res_type R = restype_break /\ res_label_in R labs then
              res_ter S2 rv'
           else (
              ifb res_type R <> restype_normal then
                res_ter S2 R
              else loop tt
           )
        ) else loop tt)
    else res_ter S1 rv).

Corollary run_javascript_correct_num : forall num p o,
  run_javascript (runs num) p = result_out o ->
  red_javascript p o.

Record runs_type_correct runs :=
  make_runs_type_correct {
    runs_type_correct_expr : forall S C e o,
       runs_type_expr runs S C e = o ->
       red_expr S C (expr_basic e) o;
    runs_type_correct_stat : forall S C t o,
       runs_type_stat runs S C t = o ->
       red_stat S C (stat_basic t) o;
    runs_type_correct_prog : forall S C p o,
       runs_type_prog runs S C p = o ->
       red_prog S C (prog_basic p) o;
    runs_type_correct_call : forall S C l v vs o,
       runs_type_call runs S C l v vs = o ->
       red_expr S C (spec_call l v vs) o;
    runs_type_correct_function_has_instance : forall S C (lo lv : object_loc) o,
       runs_type_function_has_instance runs S lo lv = o ->
       red_expr S C (spec_function_has_instance_2 lv lo) o;
    runs_type_correct_stat_while : forall S C rv ls e t o,
       runs_type_stat_while runs S C rv ls e t = o ->
       red_stat S C (stat_while_1 ls e t rv) o;
    runs_type_correct_stat_do_while : forall S C rv ls e t o,
       runs_type_stat_do_while runs S C rv ls e t = o ->
       red_stat S C (stat_do_while_1 ls t e rv) o;
    runs_type_correct_stat_for_loop : forall S C labs rv eo2 eo3 t o,
       runs_type_stat_for_loop runs S C labs rv eo2 eo3 t = o ->
       red_stat S C (stat_for_2 labs rv eo2 eo3 t) o;
    runs_type_correct_object_delete : forall S C l x str o,
       runs_type_object_delete runs S C l x str = o ->
       red_expr S C (spec_object_delete l x str) o;
    runs_type_correct_object_get_own_prop : forall S C l x sp,
       runs_type_object_get_own_prop runs S C l x = result_some sp ->
       red_spec S C (spec_object_get_own_prop l x) sp;
    runs_type_correct_object_get_prop : forall S C l x sp,
       runs_type_object_get_prop runs S C l x = result_some sp ->
       red_spec S C (spec_object_get_prop l x) sp;
    runs_type_correct_object_get : forall S C l x o,
       runs_type_object_get runs S C l x = o ->
       red_expr S C (spec_object_get l x) o;
    runs_type_correct_object_proto_is_prototype_of : forall S C lthis l o,
       runs_type_object_proto_is_prototype_of runs S lthis l = o ->
       red_expr S C (spec_call_object_proto_is_prototype_of_2_3 lthis l) o;
    runs_type_correct_object_put : forall S C l x v str o,
       runs_type_object_put runs S C l x v str = o ->
       red_expr S C (spec_object_put l x v str) o;
    runs_type_correct_equal : forall S C v1 v2 o,
       runs_type_equal runs S C v1 v2 = o ->
       red_expr S C (spec_equal v1 v2) o;
    runs_type_correct_to_integer : forall S C v o,
       runs_type_to_integer runs S C v = o ->
       red_expr S C (spec_to_integer v) o;
    runs_type_correct_to_string : forall S C v o,
       runs_type_to_string runs S C v = o ->
       red_expr S C (spec_to_string v) o
  }.

Lemma run_stat_while_correct : forall runs S C rv ls e t o,
  runs_type_correct runs ->
  run_stat_while runs S C rv ls e t = o ->
  red_stat S C (stat_while_1 ls e t rv) o.
Proof.
  intros runs IH ls e t S C rv o R. unfolds in R.
  run_pre. lets (y1&R2&K): if_spec_post_to_bool (rm R1) (rm R).
   applys~ red_stat_while_1 (rm R2). run_post_if_spec_ter_post_bool K.
    case_if.
    run red_stat_while_2_true.
     let_name. let_simpl. applys red_stat_while_3 rv'. case_if; case_if*.
     case_if in K.
       applys red_stat_while_4_not_continue. rew_logic*. case_if in K.
         run_inv. applys* red_stat_while_5_break.
         applys* red_stat_while_5_not_break. case_if in K; run_inv.
           applys* red_stat_while_6_abort.
           applys* red_stat_while_6_normal. run_hyp*.
       rew_logic in *. applys* red_stat_while_4_continue. run_hyp*.
   run_inv. applys red_stat_while_2_false.