(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, 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.     *)
(*                                                                     *)
(* *********************************************************************)

(* * Dynamic semantics for the Clight language *)

(*include "Coqlib.ma".*)
(*include "Errors.ma".*)
(*include "Integers.ma".*)
(*include "Floats.ma".*)
(*include "Values.ma".*)
(*include "AST.ma".*)
(*include "Mem.ma".*)
include "common/Globalenvs.ma".
include "Clight/Csyntax.ma".
(*include "Events.ma".*)
include "common/Smallstep.ma".

(* * * Semantics of type-dependent operations *)

(* * Interpretation of values as truth values.
  Non-zero integers, non-zero floats and non-null pointers are
  considered as true.  The integer zero (which also represents
  the null pointer) and the float 0.0 are false. *)

inductive is_false: val → type → Prop ≝
  | is_false_int: ∀sz,sg.
      is_false (Vint sz (zero ?)) (Tint sz sg)
  | is_false_pointer: ∀r,r',t.
      is_false (Vnull r) (Tpointer r' t)
 | is_false_float: ∀sz.
      is_false (Vfloat Fzero) (Tfloat sz).

inductive is_true: val → type → Prop ≝
  | is_true_int_int: ∀sz,sg,n.
      n ≠ (zero ?) →
      is_true (Vint sz n) (Tint sz sg)
  | is_true_pointer_pointer: ∀ptr,s,t.
      is_true (Vptr ptr) (Tpointer s t)
  | is_true_float: ∀f,sz.
      f ≠ Fzero →
      is_true (Vfloat f) (Tfloat sz).

inductive bool_of_val : val → type → val → Prop ≝
  | bool_of_val_true: ∀v,ty. 
         is_true v ty → 
         bool_of_val v ty Vtrue
  | bool_of_val_false: ∀v,ty.
        is_false v ty →
        bool_of_val v ty Vfalse.

(* * The following [sem_] functions compute the result of an operator
  application.  Since operators are overloaded, the result depends
  both on the static types of the arguments and on their run-time values.
  Unlike in C, automatic conversions between integers and floats
  are not performed.  For instance, [e1 + e2] is undefined if [e1]
  is a float and [e2] an integer.  The Clight producer must have explicitly
  promoted [e2] to a float. *)

let rec sem_neg (v: val) (ty: type) : option val ≝
  match ty with
  [ Tint sz _ ⇒
      match v with
      [ Vint sz' n ⇒ if eq_intsize sz sz'
                     then Some ? (Vint ? (two_complement_negation ? n))
                     else None ?
      | _ ⇒ None ?
      ]
  | Tfloat _ ⇒
      match v with
      [ Vfloat f ⇒ Some ? (Vfloat (Fneg f))
      | _ ⇒ None ?
      ]
  | _ ⇒ None ?
  ].

let rec sem_notint (v: val) : option val ≝
  match v with
  [ Vint sz n ⇒ Some ? (Vint ? (exclusive_disjunction_bv ? n (mone ?))) (* XXX *)
  | _ ⇒ None ?
  ].

let rec sem_notbool (v: val) (ty: type) : option val ≝
  match ty with
  [ Tint sz _ ⇒
      match v with
      [ Vint sz' n ⇒ if eq_intsize sz sz'
                     then Some ? (of_bool (eq_bv ? n (zero ?)))
                     else None ?
      | _ ⇒ None ?
      ]
  | Tpointer _ _ ⇒
      match v with
      [ Vptr _ ⇒ Some ? Vfalse
      | Vnull _ ⇒ Some ? Vtrue
      | _ ⇒ None ?
      ]
  | Tfloat _ ⇒
      match v with
      [ Vfloat f ⇒ Some ? (of_bool (Fcmp Ceq f Fzero))
      | _ ⇒ None ?
      ]
  | _ ⇒ None ?
  ].

let rec sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
  match classify_add t1 t2 with 
  [ add_case_ii ⇒                       (**r integer addition *)
      match v1 with 
      [ Vint sz1 n1 ⇒ match v2 with
        [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
                        (λn1. Some ? (Vint ? (addition_n ? n1 n2))) (None ?)
        | _ ⇒ None ? ]
      | _ ⇒ None ? ]
  | add_case_ff ⇒                       (**r float addition *)
      match v1 with
      [ Vfloat n1 ⇒ match v2 with
        [ Vfloat n2 ⇒ Some ? (Vfloat (Fadd n1 n2))
        | _ ⇒ None ? ]
      | _ ⇒ None ? ]
  | add_case_pi ty ⇒                    (**r pointer plus integer *)
      match v1 with
      [ Vptr ptr1 ⇒ match v2 with
        [ Vint sz2 n2 ⇒ Some ? (Vptr (shift_pointer_n ? ptr1 (sizeof ty) n2))
        | _ ⇒ None ? ]
      | Vnull r ⇒ match v2 with
        [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ?
        | _ ⇒ None ? ]
      | _ ⇒ None ? ]
  | add_case_ip ty ⇒                    (**r integer plus pointer *)
      match v1 with
      [ Vint sz1 n1 ⇒ match v2 with
        [ Vptr ptr2 ⇒ Some ? (Vptr (shift_pointer_n ? ptr2 (sizeof ty) n1))
        | Vnull r ⇒ if eq_bv ? n1 (zero ?) then Some ? (Vnull r) else None ?
        | _ ⇒ None ? ]
      | _ ⇒ None ? ]
  | add_default ⇒ None ?
].

let rec sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
  match classify_sub t1 t2 with
  [ sub_case_ii ⇒                (**r integer subtraction *)
      match v1 with
      [ Vint sz1 n1 ⇒ match v2 with
        [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1 
                        (λn1.Some ? (Vint sz2 (subtraction ? n1 n2))) (None ?)
        | _ ⇒ None ? ]
      | _ ⇒ None ? ]
  | sub_case_ff ⇒                (**r float subtraction *)
      match v1 with
      [ Vfloat f1 ⇒ match v2 with
        [ Vfloat f2 ⇒ Some ? (Vfloat (Fsub f1 f2))
        | _ ⇒ None ? ]
      | _ ⇒ None ? ]
  | sub_case_pi ty ⇒             (**r pointer minus integer *)
      match v1 with
      [ Vptr ptr1 ⇒ match v2 with
        [ Vint sz2 n2 ⇒ Some ? (Vptr (neg_shift_pointer_n ? ptr1 (sizeof ty) n2))
        | _ ⇒ None ? ]
      | Vnull r ⇒ match v2 with
        [ Vint sz2 n2 ⇒ if eq_bv ? n2 (zero ?) then Some ? (Vnull r) else None ?
        | _ ⇒ None ? ]
      | _ ⇒ None ? ]
  | sub_case_pp ty ⇒             (**r pointer minus pointer *)
      match v1 with
      [ Vptr ptr1 ⇒ match v2 with
        [ Vptr ptr2 ⇒
          if eq_block (pblock ptr1) (pblock ptr2) then
            if eqb (sizeof ty) 0 then None ?
            else match division_u ? (sub_offset ? (poff ptr1) (poff ptr2)) (repr (sizeof ty)) with
                 [ None ⇒ None ?
                 | Some v ⇒ Some ? (Vint I32 v) (* XXX choose size from result type? *)
                 ]
          else None ?
        | _ ⇒ None ? ]
      | Vnull r ⇒ match v2 with [ Vnull r' ⇒ Some ? (Vint I32 (*XXX*) (zero ?)) | _ ⇒ None ? ]
      | _ ⇒ None ? ]
  | sub_default ⇒ None ?
  ].

let rec sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
 match classify_mul t1 t2 with
  [ mul_case_ii ⇒
      match v1 with
      [ Vint sz1 n1 ⇒ match v2 with
          [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
                          (λn1. Some ? (Vint sz2 (\snd (split ??? (multiplication ? n1 n2))))) (None ?)
        | _ ⇒ None ? ]
      | _ ⇒ None ? ]
  | mul_case_ff ⇒
      match v1 with
      [ Vfloat f1 ⇒ match v2 with
        [ Vfloat f2 ⇒ Some ? (Vfloat (Fmul f1 f2))
        | _ ⇒ None ? ]
      | _ ⇒ None ? ]
  | mul_default ⇒
      None ?
].

let rec sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
  match classify_div t1 t2 with
  [ div_case_I32unsi ⇒
      match v1 with
      [ Vint sz1 n1 ⇒ match v2 with
        [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
                        (λn1. option_map … (Vint ?) (division_u ? n1 n2)) (None ?)
        | _ ⇒ None ? ]
      | _ ⇒ None ? ]
  | div_case_ii ⇒
      match v1 with
       [ Vint sz1 n1 ⇒ match v2 with
         [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
                         (λn1. option_map … (Vint ?) (division_s ? n1 n2)) (None ?)
         | _ ⇒ None ? ]
      | _ ⇒ None ? ]
  | div_case_ff ⇒
      match v1 with
      [ Vfloat f1 ⇒ match v2 with
        [ Vfloat f2 ⇒ Some ? (Vfloat(Fdiv f1 f2))
        | _ ⇒ None ? ]
      | _ ⇒ None ? ]
  | div_default ⇒
      None ?
  ].

let rec sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
  match classify_mod t1 t2 with
  [ mod_case_I32unsi ⇒
      match v1 with
      [ Vint sz1 n1 ⇒ match v2 with
        [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
                        (λn1. option_map … (Vint ?) (modulus_u ? n1 n2)) (None ?)
        | _ ⇒ None ? ]
      | _ ⇒ None ? ]
  | mod_case_ii ⇒
      match v1 with
      [ Vint sz1 n1 ⇒ match v2 with
        [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
                        (λn1. option_map … (Vint ?) (modulus_s ? n1 n2)) (None ?)
        | _ ⇒ None ? ]
      | _ ⇒ None ? ]
  | mod_default ⇒
      None ?
  ].

let rec sem_and (v1,v2: val) : option val ≝
  match v1 with
  [ Vint sz1 n1 ⇒ match v2 with
    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
                    (λn1. Some ? (Vint ? (conjunction_bv ? n1 n2))) (None ?)
    | _ ⇒ None ? ]
  | _ ⇒ None ?
  ].

let rec sem_or (v1,v2: val) : option val ≝
  match v1 with
  [ Vint sz1 n1 ⇒ match v2 with
    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
                    (λn1. Some ? (Vint ? (inclusive_disjunction_bv ? n1 n2))) (None ?)
    | _ ⇒ None ? ]
  | _ ⇒ None ?
  ].

let rec sem_xor (v1,v2: val) : option val ≝
  match v1 with
  [ Vint sz1 n1 ⇒ match v2 with
    [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
                    (λn1. Some ? (Vint ? (exclusive_disjunction_bv ? n1 n2))) (None ?)
    | _ ⇒ None ? ]
  | _ ⇒ None ?
  ].

let rec sem_shl (v1,v2: val): option val ≝
  match v1 with
  [ Vint sz1 n1 ⇒ match v2 with
    [ Vint sz2 n2 ⇒
        if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
        then Some ? (Vint sz1 (shift_left ?? (nat_of_bitvector … n2) n1 false))
        else None ?
    | _ ⇒ None ? ]
  | _ ⇒ None ? ].

let rec sem_shr (v1: val) (t1: type) (v2: val) (t2: type): option val ≝
  match classify_shr t1 t2 with 
  [ shr_case_I32unsi ⇒
      match v1 with 
      [ Vint sz1 n1 ⇒ match v2 with
        [ Vint sz2 n2 ⇒
            if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
            then Some ? (Vint ? (shift_right ?? (nat_of_bitvector … n2) n1 false))
            else None ?
        | _ ⇒ None ? ]
      | _ ⇒ None ? ]
   | shr_case_ii => 
      match v1 with 
      [ Vint sz1 n1 ⇒ match v2 with
        [ Vint sz2 n2 ⇒
            if lt_u ? n2 (bitvector_of_nat … (bitsize_of_intsize sz1))
            then Some ? (Vint ? (shift_right ?? (nat_of_bitvector … n2) n1 (head' … n1)))
            else None ?
        | _ ⇒ None ? ]
      | _ ⇒ None ? ]
   | shr_default ⇒
      None ?
   ].

let rec sem_cmp_mismatch (c: comparison): option val ≝
  match c with
  [ Ceq =>  Some ? Vfalse
  | Cne =>  Some ? Vtrue
  | _   => None ?
  ].

let rec sem_cmp_match (c: comparison): option val ≝
  match c with
  [ Ceq =>  Some ? Vtrue
  | Cne =>  Some ? Vfalse
  | _   => None ?
  ].
  
let rec sem_cmp (c:comparison)
                  (v1: val) (t1: type) (v2: val) (t2: type)
                  (m: mem): option val ≝
  match classify_cmp t1 t2 with
  [ cmp_case_I32unsi ⇒
      match v1 with
      [ Vint sz1 n1 ⇒ match v2 with
        [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
                        (λn1. Some ? (of_bool (cmpu_int ? c n1 n2))) (None ?)
        | _ ⇒ None ? ]
      | _ ⇒ None ? ]
  | cmp_case_ii ⇒
      match v1 with
      [ Vint sz1 n1 ⇒ match v2 with
         [ Vint sz2 n2 ⇒ intsize_eq_elim ? sz1 sz2 ? n1
                         (λn1. Some ? (of_bool (cmp_int ? c n1 n2))) (None ?)
         | _ ⇒ None ?
         ]
      | _ ⇒ None ?      
      ]
  | cmp_case_pp ⇒
      match v1 with
      [ Vptr ptr1 ⇒
        match v2 with
        [ Vptr ptr2 ⇒
          if valid_pointer m ptr1
          ∧ valid_pointer m ptr2 then
            if eq_block (pblock ptr1) (pblock ptr2)
            then Some ? (of_bool (cmp_offset c (poff ptr1) (poff ptr2)))
            else sem_cmp_mismatch c
          else None ?
        | Vnull r2 ⇒ sem_cmp_mismatch c
        | _ ⇒ None ? ]
      | Vnull r1 ⇒
        match v2 with
        [ Vptr ptr2 ⇒ sem_cmp_mismatch c
        | Vnull r2 ⇒ sem_cmp_match c
        | _ ⇒ None ?
        ]
      | _ ⇒ None ? ]
  | cmp_case_ff ⇒
      match v1 with
      [ Vfloat f1 ⇒
        match v2 with
        [ Vfloat f2 ⇒ Some ? (of_bool (Fcmp c f1 f2))
        | _ ⇒ None ? ]
      | _ ⇒ None ? ]
  | cmp_default ⇒ None ?
  ].

definition sem_unary_operation
            : unary_operation → val → type → option val ≝
  λop,v,ty.
  match op with
  [ Onotbool => sem_notbool v ty
  | Onotint => sem_notint v
  | Oneg => sem_neg v ty
  ].

let rec sem_binary_operation
    (op: binary_operation)
    (v1: val) (t1: type) (v2: val) (t2:type)
    (m: mem): option val ≝
  match op with
  [ Oadd ⇒ sem_add v1 t1 v2 t2
  | Osub ⇒ sem_sub v1 t1 v2 t2 
  | Omul ⇒ sem_mul v1 t1 v2 t2
  | Omod ⇒ sem_mod v1 t1 v2 t2
  | Odiv ⇒ sem_div v1 t1 v2 t2
  | Oand ⇒ sem_and v1 v2  
  | Oor  ⇒ sem_or v1 v2 
  | Oxor ⇒ sem_xor v1 v2 
  | Oshl ⇒ sem_shl v1 v2
  | Oshr ⇒ sem_shr v1 t1 v2 t2
  | Oeq ⇒ sem_cmp Ceq v1 t1 v2 t2 m
  | One ⇒ sem_cmp Cne v1 t1 v2 t2 m
  | Olt ⇒ sem_cmp Clt v1 t1 v2 t2 m
  | Ogt ⇒ sem_cmp Cgt v1 t1 v2 t2 m
  | Ole ⇒ sem_cmp Cle v1 t1 v2 t2 m
  | Oge ⇒ sem_cmp Cge v1 t1 v2 t2 m
  ].

(* * Semantic of casts.  [cast v1 t1 t2 v2] holds if value [v1],
  viewed with static type [t1], can be cast to type [t2],
  resulting in value [v2].  *)

let rec cast_int_int (sz: intsize) (sg: signedness) (dstsz: intsize)  (i: BitVector (bitsize_of_intsize sz)) : BitVector (bitsize_of_intsize dstsz) ≝
  match sg with [ Signed ⇒ sign_ext ?? i | Unsigned ⇒ zero_ext ?? i ].

let rec cast_int_float (si : signedness) (n:nat) (i: BitVector n) : float ≝
  match si with
  [ Signed ⇒ floatofint ? i
  | Unsigned ⇒ floatofintu ? i
  ].

let rec cast_float_int (sz : intsize) (si : signedness) (f: float) : BitVector (bitsize_of_intsize sz) ≝
  match si with
  [ Signed ⇒ intoffloat ? f
  | Unsigned ⇒ intuoffloat ? f
  ].

let rec cast_float_float (sz: floatsize) (f: float) : float ≝
  match sz with
  [ F32 ⇒ singleoffloat f
  | F64 ⇒ f
  ].

inductive type_region : type → region → Prop ≝
| type_rgn_pointer : ∀s,t. type_region (Tpointer s t) s
| type_rgn_array : ∀s,t,n. type_region (Tarray s t n) s
(* XXX Is the following necessary? *)
| type_rgn_code : ∀tys,ty. type_region (Tfunction tys ty) Code.

inductive cast : mem → val → type → type → val → Prop ≝
  | cast_ii:   ∀m,sz2,sz1,si1,si2,i.            (**r int to int  *)
      cast m (Vint sz1 i) (Tint sz1 si1) (Tint sz2 si2)
           (Vint sz2 (cast_int_int sz1 si1 sz2 i))
  | cast_fi:   ∀m,f,sz1,sz2,si2.                (**r float to int *)
      cast m (Vfloat f) (Tfloat sz1) (Tint sz2 si2)
           (Vint sz2 (cast_float_int sz2 si2 f))
  | cast_if:   ∀m,sz1,sz2,si1,i.                (**r int to float  *)
      cast m (Vint sz1 i) (Tint sz1 si1) (Tfloat sz2)
          (Vfloat (cast_float_float sz2 (cast_int_float si1 ? i)))
  | cast_ff:   ∀m,f,sz1,sz2.                    (**r float to float *)
      cast m (Vfloat f) (Tfloat sz1) (Tfloat sz2)
           (Vfloat (cast_float_float sz2 f))
  | cast_pp: ∀m,ty,ty',ptr,r'.
      type_region ty (ptype ptr) →
      type_region ty' r' →
      ∀pc':pointer_compat (pblock ptr) r'.
      cast m (Vptr ptr) ty ty' (Vptr (mk_pointer r' (pblock ptr) pc' (poff ptr)))
  | cast_ip_z: ∀m,sz,sg,ty',r.
      type_region ty' r →
      cast m (Vint sz (zero ?)) (Tint sz sg) ty' (Vnull r)
  | cast_pp_z: ∀m,ty,ty',r,r'.
      type_region ty r →
      type_region ty' r' →
      cast m (Vnull r) ty ty' (Vnull r').

(* * * Operational semantics *)

(* * The semantics uses two environments.  The global environment
  maps names of functions and global variables to memory block references,
  and function pointers to their definitions.  (See module [Globalenvs].) *)

definition genv ≝ (genv_t Genv) clight_fundef.

(* * The local environment maps local variables to block references.
  The current value of the variable is stored in the associated memory
  block. *)

definition env ≝ identifier_map SymbolTag block. (* map variable -> location *)

definition empty_env: env ≝ (empty_map …).

(* * [load_value_of_type ty m b ofs] computes the value of a datum
  of type [ty] residing in memory [m] at block [b], offset [ofs].
  If the type [ty] indicates an access by value, the corresponding
  memory load is performed.  If the type [ty] indicates an access by
  reference, the pointer [Vptr b ofs] is returned. *)

let rec load_value_of_type (ty: type) (m: mem) (b: block) (ofs: offset) : option val ≝
  match access_mode ty with
  [ By_value chunk ⇒ loadv chunk m (Vptr (mk_pointer Any b ? ofs))
  | By_reference r ⇒
    match pointer_compat_dec b r with
    [ inl p ⇒ Some ? (Vptr (mk_pointer r b p ofs))
    | inr _ ⇒ None ?
    ]
  | By_nothing ⇒ None ?
  ].
cases b //
qed.

(* * Symmetrically, [store_value_of_type ty m b ofs v] returns the
  memory state after storing the value [v] in the datum
  of type [ty] residing in memory [m] at block [b], offset [ofs].
  This is allowed only if [ty] indicates an access by value. *)

let rec store_value_of_type (ty_dest: type) (m: mem) (loc: block) (ofs: offset) (v: val) : option mem ≝
  match access_mode ty_dest with
  [ By_value chunk ⇒ storev chunk m (Vptr (mk_pointer Any loc ? ofs)) v
  | By_reference _ ⇒ None ?
  | By_nothing ⇒ None ?
  ].
cases loc //
qed.

(* * Allocation of function-local variables.
  [alloc_variables e1 m1 vars e2 m2] allocates one memory block
  for each variable declared in [vars], and associates the variable
  name with this block.  [e1] and [m1] are the initial local environment
  and memory state.  [e2] and [m2] are the final local environment
  and memory state. *)

inductive alloc_variables: env → mem →
                            list (ident × type) →
                            env → mem → Prop ≝
  | alloc_variables_nil:
      ∀e,m.
      alloc_variables e m (nil ?) e m
  | alloc_variables_cons:
      ∀e,m,id,ty,vars,m1,b1,m2,e2.
      alloc m 0 (sizeof ty) Any = 〈m1, b1〉 →
      alloc_variables (add … e id b1) m1 vars e2 m2 →
      alloc_variables e m (〈id, ty〉 :: vars) e2 m2.

(* * Initialization of local variables that are parameters to a function.
  [bind_parameters e m1 params args m2] stores the values [args]
  in the memory blocks corresponding to the variables [params].
  [m1] is the initial memory state and [m2] the final memory state. *)

inductive bind_parameters: env →
                           mem → list (ident × type) → list val →
                           mem → Prop ≝
  | bind_parameters_nil:
      ∀e,m.
      bind_parameters e m (nil ?) (nil ?) m
  | bind_parameters_cons:
      ∀e,m,id,ty,params,v1,vl,b,m1,m2.
      lookup ?? e id = Some ? b →
      store_value_of_type ty m b zero_offset v1 = Some ? m1 →
      bind_parameters e m1 params vl m2 →
      bind_parameters e m (〈id, ty〉 :: params) (v1 :: vl) m2.

(* * Return the list of blocks in the codomain of [e]. *)

definition blocks_of_env : env → list block ≝ λe.
  map ?? (λx. snd ?? x) (elements ?? e).

(* * Selection of the appropriate case of a [switch], given the value [n]
  of the selector expression. *)
(* FIXME: now that we have several sizes of integer, it isn't clear whether we
   should allow case labels to be of a different size to the switch expression. *)
let rec select_switch (sz:intsize) (n: BitVector (bitsize_of_intsize sz)) (sl: labeled_statements)
                       on sl : labeled_statements ≝
  match sl with
  [ LSdefault _ ⇒ sl
  | LScase sz' c s sl' ⇒ intsize_eq_elim ? sz sz' ? n
                         (λn. if eq_bv ? c n then sl else select_switch sz' n sl') (select_switch sz n sl')
  ].

(* * Turn a labeled statement into a sequence *)

let rec seq_of_labeled_statement (sl: labeled_statements) : statement ≝
  match sl with
  [ LSdefault s ⇒ s
  | LScase _ c s sl' ⇒ Ssequence s (seq_of_labeled_statement sl')
  ].

(*
Section SEMANTICS.

Variable ge: genv.

(** ** Evaluation of expressions *)

Section EXPR.

Variable e: env.
Variable m: mem.
*)
(* * [eval_expr ge e m a v] defines the evaluation of expression [a]
  in r-value position.  [v] is the value of the expression.
  [e] is the current environment and [m] is the current memory state. *)

inductive eval_expr (ge:genv) (e:env) (m:mem) : expr → val → trace → Prop ≝
  | eval_Econst_int:   ∀sz,sg,i.
      eval_expr ge e m (Expr (Econst_int sz i) (Tint sz sg)) (Vint sz i) E0
  | eval_Econst_float:   ∀f,ty.
      eval_expr ge e m (Expr (Econst_float f) ty) (Vfloat f) E0
  | eval_Elvalue: ∀a,ty,loc,ofs,v,tr.
      eval_lvalue ge e m (Expr a ty) loc ofs tr →
      load_value_of_type ty m loc ofs = Some ? v →
      eval_expr ge e m (Expr a ty) v tr
  | eval_Eaddrof: ∀a,ty,r,loc,ofs,tr.
      eval_lvalue ge e m a loc ofs tr →
      ∀pc:pointer_compat loc r.
      eval_expr ge e m (Expr (Eaddrof a) (Tpointer r ty)) (Vptr (mk_pointer r loc pc ofs)) tr
  | eval_Esizeof: ∀ty',sz,sg.
      eval_expr ge e m (Expr (Esizeof ty') (Tint sz sg)) (Vint sz (repr ? (sizeof ty'))) E0
  | eval_Eunop:  ∀op,a,ty,v1,v,tr.
      eval_expr ge e m a v1 tr →
      sem_unary_operation op v1 (typeof a) = Some ? v →
      eval_expr ge e m (Expr (Eunop op a) ty) v tr
  | eval_Ebinop: ∀op,a1,a2,ty,v1,v2,v,tr1,tr2.
      eval_expr ge e m a1 v1 tr1 →
      eval_expr ge e m a2 v2 tr2 →
      sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m = Some ? v →
      eval_expr ge e m (Expr (Ebinop op a1 a2) ty) v (tr1⧺tr2)
  | eval_Econdition_true: ∀a1,a2,a3,ty,v1,v2,tr1,tr2.
      eval_expr ge e m a1 v1 tr1 →
      is_true v1 (typeof a1) →
      eval_expr ge e m a2 v2 tr2 →
      eval_expr ge e m (Expr (Econdition a1 a2 a3) ty) v2 (tr1⧺tr2)
  | eval_Econdition_false: ∀a1,a2,a3,ty,v1,v3,tr1,tr2.
      eval_expr ge e m a1 v1 tr1 →
      is_false v1 (typeof a1) →
      eval_expr ge e m a3 v3 tr2 →
      eval_expr ge e m (Expr (Econdition a1 a2 a3) ty) v3 (tr1⧺tr2)
  | eval_Eorbool_1: ∀a1,a2,ty,v1,tr.
      eval_expr ge e m a1 v1 tr →
      is_true v1 (typeof a1) →
      eval_expr ge e m (Expr (Eorbool a1 a2) ty) Vtrue tr
  | eval_Eorbool_2: ∀a1,a2,ty,v1,v2,v,tr1,tr2.
      eval_expr ge e m a1 v1 tr1 →
      is_false v1 (typeof a1) →
      eval_expr ge e m a2 v2 tr2 →
      bool_of_val v2 (typeof a2) v →
      eval_expr ge e m (Expr (Eorbool a1 a2) ty) v (tr1⧺tr2)
  | eval_Eandbool_1: ∀a1,a2,ty,v1,tr.
      eval_expr ge e m a1 v1 tr →
      is_false v1 (typeof a1) →
      eval_expr ge e m (Expr (Eandbool a1 a2) ty) Vfalse tr
  | eval_Eandbool_2: ∀a1,a2,ty,v1,v2,v,tr1,tr2.
      eval_expr ge e m a1 v1 tr1 →
      is_true v1 (typeof a1) →
      eval_expr ge e m a2 v2 tr2 →
      bool_of_val v2 (typeof a2) v →
      eval_expr ge e m (Expr (Eandbool a1 a2) ty) v (tr1⧺tr2)
  | eval_Ecast:   ∀a,ty,ty',v1,v,tr.
      eval_expr ge e m a v1 tr →
      cast m v1 (typeof a) ty v →
      eval_expr ge e m (Expr (Ecast ty a) ty') v tr
  | eval_Ecost: ∀a,ty,v,l,tr.
      eval_expr ge e m a v tr →
      eval_expr ge e m (Expr (Ecost l a) ty) v (tr⧺Echarge l)

(* * [eval_lvalue ge e m a r b ofs] defines the evaluation of expression [a]
  in l-value position.  The result is the memory location [b, ofs]
  that contains the value of the expression [a].  The memory location should
  be representable in a pointer of region r. *)

with eval_lvalue (*(ge:genv) (e:env) (m:mem)*) : expr → block → offset → trace → Prop ≝
  | eval_Evar_local:   ∀id,l,ty.
      (* XXX notation? e!id*) lookup ?? e id = Some ? l →
      eval_lvalue ge e m (Expr (Evar id) ty) l zero_offset E0
  | eval_Evar_global: ∀id,l,ty.
      (* XXX e!id *) lookup ?? e id = None ? →
      find_symbol ?? ge id = Some ? l →
      eval_lvalue ge e m (Expr (Evar id) ty) l zero_offset E0
  | eval_Ederef: ∀a,ty,r,l,p,ofs,tr.
      eval_expr ge e m a (Vptr (mk_pointer r l p ofs)) tr →
      eval_lvalue ge e m (Expr (Ederef a) ty) l ofs tr
    (* Aside: note that each block of memory is entirely contained within one
       memory region; hence adding a field offset will not produce a location
       outside of the original location's region. *)
 | eval_Efield_struct:   ∀a,i,ty,l,ofs,id,fList,delta,tr.
      eval_lvalue ge e m a l ofs tr →
      typeof a = Tstruct id fList →
      field_offset i fList = OK ? delta →
      eval_lvalue ge e m (Expr (Efield a i) ty) l (shift_offset ? ofs (repr I32 delta)) tr
 | eval_Efield_union:   ∀a,i,ty,l,ofs,id,fList,tr.
      eval_lvalue ge e m a l ofs tr →
      typeof a = Tunion id fList →
      eval_lvalue ge e m (Expr (Efield a i) ty) l ofs tr.

let rec eval_expr_ind (ge:genv) (e:env) (m:mem)
  (P:∀a,v,tr. eval_expr ge e m a v tr → Prop)
  (eci:∀sz,sg,i. P ??? (eval_Econst_int ge e m sz sg i))
  (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
  (elv:∀a,ty,loc,ofs,v,tr,H1,H2. P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2))
  (ead:∀a,ty,r,loc,pc,ofs,tr,H. P ??? (eval_Eaddrof ge e m a ty r loc pc ofs tr H))
  (esz:∀ty',sz,sg. P ??? (eval_Esizeof ge e m ty' sz sg))
  (eun:∀op,a,ty,v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Eunop ge e m op a ty v1 v tr H1 H2))
  (ebi:∀op,a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a2 v2 tr2 H2 → P ??? (eval_Ebinop ge e m op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3))
  (ect:∀a1,a2,a3,ty,v1,v2,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Econdition_true ge e m a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3))
  (ecf:∀a1,a2,a3,ty,v1,v3,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a3 v3 tr2 H3 → P ??? (eval_Econdition_false ge e m a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3))
  (eo1:∀a1,a2,ty,v1,tr,H1,H2. P a1 v1 tr H1 → P ??? (eval_Eorbool_1 ge e m a1 a2 ty v1 tr H1 H2))
  (eo2:∀a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3,H4. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eorbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4))
  (ea1:∀a1,a2,ty,v1,tr,H1,H2. P a1 v1 tr H1 → P ??? (eval_Eandbool_1 ge e m a1 a2 ty v1 tr H1 H2))
  (ea2:∀a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3,H4. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eandbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4))
  (ecs:∀a,ty,ty',v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Ecast ge e m a ty ty' v1 v tr H1 H2))
  (eco:∀a,ty,v,l,tr,H. P a v tr H → P ??? (eval_Ecost ge e m a ty v l tr H))
  (a:expr) (v:val) (tr:trace) (ev:eval_expr ge e m a v tr) on ev : P a v tr ev ≝
  match ev with
  [ eval_Econst_int sz sg i ⇒ eci sz sg i
  | eval_Econst_float f ty ⇒ ecF f ty
  | eval_Elvalue a ty loc ofs v tr H1 H2 ⇒ elv a ty loc ofs v tr H1 H2
  | eval_Eaddrof a ty r loc pc ofs tr H ⇒ ead a ty r loc pc ofs tr H
  | eval_Esizeof ty' sz sg ⇒ esz ty' sz sg
  | eval_Eunop op a ty v1 v tr H1 H2 ⇒ eun op a ty v1 v tr H1 H2 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v1 tr H1)
  | eval_Ebinop op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 ⇒ ebi op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H2)
  | eval_Econdition_true a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3 ⇒ ect a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H3)
  | eval_Econdition_false a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3 ⇒ ecf a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a3 v3 tr2 H3)
  | eval_Eorbool_1 a1 a2 ty v1 tr H1 H2 ⇒ eo1 a1 a2 ty v1 tr H1 H2 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr H1)
  | eval_Eorbool_2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 ⇒ eo2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H3)
  | eval_Eandbool_1 a1 a2 ty v1 tr H1 H2 ⇒ ea1 a1 a2 ty v1 tr H1 H2 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr H1)
  | eval_Eandbool_2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 ⇒ ea2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr1 H1) (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H3)
  | eval_Ecast a ty ty' v1 v tr H1 H2 ⇒ ecs a ty ty' v1 v tr H1 H2 (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v1 tr H1)
  | eval_Ecost a ty v l tr H ⇒ eco a ty v l tr H (eval_expr_ind ge e m P eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v tr H)
  ].

inverter eval_expr_inv_ind for eval_expr : Prop.

let rec eval_lvalue_ind (ge:genv) (e:env) (m:mem)
  (P:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop)
  (lvl:∀id,l,ty,H. P ???? (eval_Evar_local ge e m id l ty H))
  (lvg:∀id,l,ty,H1,H2. P ???? (eval_Evar_global ge e m id l ty H1 H2))
  (lde:∀a,ty,r,l,pc,ofs,tr,H. P ???? (eval_Ederef ge e m a ty r l pc ofs tr H))
  (lfs:∀a,i,ty,l,ofs,id,fList,delta,tr,H1,H2,H3. P a l ofs tr H1 → P ???? (eval_Efield_struct ge e m a i ty l ofs id fList delta tr H1 H2 H3))
  (lfu:∀a,i,ty,l,ofs,id,fList,tr,H1,H2. P a l ofs tr H1 → P ???? (eval_Efield_union ge e m a i ty l ofs id fList tr H1 H2))
  (a:expr) (loc:block) (ofs:offset) (tr:trace) (ev:eval_lvalue ge e m a loc ofs tr) on ev : P a loc ofs tr ev ≝
  match ev with
  [ eval_Evar_local id l ty H ⇒ lvl id l ty H
  | eval_Evar_global id l ty H1 H2 ⇒ lvg id l ty H1 H2
  | eval_Ederef a ty r l pc ofs tr H ⇒ lde a ty r l pc ofs tr H 
  | eval_Efield_struct a i ty l ofs id fList delta tr H1 H2 H3 ⇒ lfs a i ty l ofs id fList delta tr H1 H2 H3 (eval_lvalue_ind ge e m P lvl lvg lde lfs lfu a l ofs tr H1)
  | eval_Efield_union a i ty l ofs id fList tr H1 H2 ⇒ lfu a i ty l ofs id fList tr H1 H2 (eval_lvalue_ind ge e m P lvl lvg lde lfs lfu a l ofs tr H1)
  ].

(*
ninverter eval_lvalue_inv_ind for eval_lvalue : Prop.
*)

definition eval_lvalue_inv_ind :
  ∀x1: genv.
   ∀x2: env.
    ∀x3: mem.
     ∀x4: expr.
       ∀x6: block.
        ∀x7: offset.
         ∀x8: trace.
          ∀P:
            ∀_z1430: expr.
              ∀_z1428: block. ∀_z1427: offset. ∀_z1426: trace. Prop.
           ∀_H1: ?.
            ∀_H2: ?.
             ∀_H3: ?.
              ∀_H4: ?.
               ∀_H5: ?.
                ∀_Hterm: eval_lvalue x1 x2 x3 x4 x6 x7 x8.
                 P x4 x6 x7 x8
:=
  (λx1:genv.
    (λx2:env.
      (λx3:mem.
        (λx4:expr.
            (λx6:block.
              (λx7:offset.
                (λx8:trace.
                  (λP:∀_z1430: expr.
                         ∀_z1428: block.
                          ∀_z1427: offset. ∀_z1426: trace. Prop.
                    (λH1:?.
                      (λH2:?.
                        (λH3:?.
                          (λH4:?.
                            (λH5:?.
                              (λHterm:eval_lvalue x1 x2 x3 x4 x6 x7 x8.
                                ((λHcut:∀z1435: eq expr x4 x4.
                                           ∀z1433: eq block x6 x6.
                                            ∀z1432: eq offset x7 x7.
                                             ∀z1431: eq trace x8 x8.
                                              P x4 x6 x7 x8.
                                   (Hcut (refl expr x4)
                                     (refl block x6)
                                     (refl offset x7) (refl trace x8)))
                                  ?))))))))))))))).
[ @(eval_lvalue_ind x1 x2 x3 (λa,loc,ofs,tr,e. ∀e1:eq ? x4 a. ∀e3:eq ? x6 loc. ∀e4:eq ? x7 ofs. ∀e5:eq ? x8 tr. P a loc ofs tr) … Hterm)
  [ @H1 | @H2 | @H3 | @H4 | @H5 ]
| *: skip
] qed.

let rec eval_expr_ind2 (ge:genv) (e:env) (m:mem)
  (P:∀a,v,tr. eval_expr ge e m a v tr → Prop)
  (Q:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop)
  (eci:∀sz,sg,i. P ??? (eval_Econst_int ge e m sz sg i))
  (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
  (elv:∀a,ty,loc,ofs,v,tr,H1,H2. Q (Expr a ty) loc ofs tr H1 → P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2))
  (ead:∀a,ty,r,loc,pc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty r loc ofs tr H pc))
  (esz:∀ty',sz,sg. P ??? (eval_Esizeof ge e m ty' sz sg))
  (eun:∀op,a,ty,v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Eunop ge e m op a ty v1 v tr H1 H2))
  (ebi:∀op,a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a2 v2 tr2 H2 → P ??? (eval_Ebinop ge e m op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3))
  (ect:∀a1,a2,a3,ty,v1,v2,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Econdition_true ge e m a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3))
  (ecf:∀a1,a2,a3,ty,v1,v3,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a3 v3 tr2 H3 → P ??? (eval_Econdition_false ge e m a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3))
  (eo1:∀a1,a2,ty,v1,tr,H1,H2. P a1 v1 tr H1 → P ??? (eval_Eorbool_1 ge e m a1 a2 ty v1 tr H1 H2))
  (eo2:∀a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3,H4. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eorbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4))
  (ea1:∀a1,a2,ty,v1,tr,H1,H2. P a1 v1 tr H1 → P ??? (eval_Eandbool_1 ge e m a1 a2 ty v1 tr H1 H2))
  (ea2:∀a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3,H4. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eandbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4))
  (ecs:∀a,ty,ty',v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Ecast ge e m a ty ty' v1 v tr H1 H2))
  (eco:∀a,ty,v,l,tr,H. P a v tr H → P ??? (eval_Ecost ge e m a ty v l tr H))
  (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H))
  (lvg:∀id,l,ty,H1,H2. Q ???? (eval_Evar_global ge e m id l ty H1 H2))
  (lde:∀a,ty,r,l,pc,ofs,tr,H. P a (Vptr (mk_pointer r l pc ofs)) tr H → Q ???? (eval_Ederef ge e m a ty r l pc ofs tr H))
  (lfs:∀a,i,ty,l,ofs,id,fList,delta,tr,H1,H2,H3. Q a l ofs tr H1 → Q ???? (eval_Efield_struct ge e m a i ty l ofs id fList delta tr H1 H2 H3))
  (lfu:∀a,i,ty,l,ofs,id,fList,tr,H1,H2. Q a l ofs tr H1 → Q ???? (eval_Efield_union ge e m a i ty l ofs id fList tr H1 H2))
  
  (a:expr) (v:val) (tr:trace) (ev:eval_expr ge e m a v tr) on ev : P a v tr ev ≝
  match ev with
  [ eval_Econst_int sz sg i ⇒ eci sz sg i
  | eval_Econst_float f ty ⇒ ecF f ty
  | eval_Elvalue a ty loc ofs v tr H1 H2 ⇒ elv a ty loc ofs v tr H1 H2 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu (Expr a ty) loc ofs tr H1)
  | eval_Eaddrof a ty r loc ofs tr H pc ⇒ ead a ty r loc pc ofs tr H (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a loc ofs tr H)
  | eval_Esizeof ty' sz sg ⇒ esz ty' sz sg
  | eval_Eunop op a ty v1 v tr H1 H2 ⇒ eun op a ty v1 v tr H1 H2 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a v1 tr H1)
  | eval_Ebinop op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 ⇒ ebi op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H2)
  | eval_Econdition_true a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3 ⇒ ect a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H3)
  | eval_Econdition_false a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3 ⇒ ecf a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a3 v3 tr2 H3)
  | eval_Eorbool_1 a1 a2 ty v1 tr H1 H2 ⇒ eo1 a1 a2 ty v1 tr H1 H2 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr H1)
  | eval_Eorbool_2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 ⇒ eo2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H3)
  | eval_Eandbool_1 a1 a2 ty v1 tr H1 H2 ⇒ ea1 a1 a2 ty v1 tr H1 H2 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr H1)
  | eval_Eandbool_2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 ⇒ ea2 a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr1 H1) (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H3)
  | eval_Ecast a ty ty' v1 v tr H1 H2 ⇒ ecs a ty ty' v1 v tr H1 H2 (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a v1 tr H1)
  | eval_Ecost a ty v l tr H ⇒ eco a ty v l tr H (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a v tr H)
  ]
and eval_lvalue_ind2 (ge:genv) (e:env) (m:mem)
  (P:∀a,v,tr. eval_expr ge e m a v tr → Prop)
  (Q:∀a,loc,ofs,tr. eval_lvalue ge e m a loc ofs tr → Prop)
  (eci:∀sz,sg,i. P ??? (eval_Econst_int ge e m sz sg i))
  (ecF:∀f,ty. P ??? (eval_Econst_float ge e m f ty))
  (elv:∀a,ty,loc,ofs,v,tr,H1,H2. Q (Expr a ty) loc ofs tr H1 → P ??? (eval_Elvalue ge e m a ty loc ofs v tr H1 H2))
  (ead:∀a,ty,r,loc,pc,ofs,tr,H. Q a loc ofs tr H → P ??? (eval_Eaddrof ge e m a ty r loc ofs tr H pc))
  (esz:∀ty',sz,sg. P ??? (eval_Esizeof ge e m ty' sz sg))
  (eun:∀op,a,ty,v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Eunop ge e m op a ty v1 v tr H1 H2))
  (ebi:∀op,a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a2 v2 tr2 H2 → P ??? (eval_Ebinop ge e m op a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3))
  (ect:∀a1,a2,a3,ty,v1,v2,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Econdition_true ge e m a1 a2 a3 ty v1 v2 tr1 tr2 H1 H2 H3))
  (ecf:∀a1,a2,a3,ty,v1,v3,tr1,tr2,H1,H2,H3. P a1 v1 tr1 H1 → P a3 v3 tr2 H3 → P ??? (eval_Econdition_false ge e m a1 a2 a3 ty v1 v3 tr1 tr2 H1 H2 H3))
  (eo1:∀a1,a2,ty,v1,tr,H1,H2. P a1 v1 tr H1 → P ??? (eval_Eorbool_1 ge e m a1 a2 ty v1 tr H1 H2))
  (eo2:∀a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3,H4. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eorbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4))
  (ea1:∀a1,a2,ty,v1,tr,H1,H2. P a1 v1 tr H1 → P ??? (eval_Eandbool_1 ge e m a1 a2 ty v1 tr H1 H2))
  (ea2:∀a1,a2,ty,v1,v2,v,tr1,tr2,H1,H2,H3,H4. P a1 v1 tr1 H1 → P a2 v2 tr2 H3 → P ??? (eval_Eandbool_2 ge e m a1 a2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4))
  (ecs:∀a,ty,ty',v1,v,tr,H1,H2. P a v1 tr H1 → P ??? (eval_Ecast ge e m a ty ty' v1 v tr H1 H2))
  (eco:∀a,ty,v,l,tr,H. P a v tr H → P ??? (eval_Ecost ge e m a ty v l tr H))
  (lvl:∀id,l,ty,H. Q ???? (eval_Evar_local ge e m id l ty H))
  (lvg:∀id,l,ty,H1,H2. Q ???? (eval_Evar_global ge e m id l ty H1 H2))
  (lde:∀a,ty,r,l,pc,ofs,tr,H. P a (Vptr (mk_pointer r l pc ofs)) tr H → Q ???? (eval_Ederef ge e m a ty r l pc ofs tr H))
  (lfs:∀a,i,ty,l,ofs,id,fList,delta,tr,H1,H2,H3. Q a l ofs tr H1 → Q ???? (eval_Efield_struct ge e m a i ty l ofs id fList delta tr H1 H2 H3))
  (lfu:∀a,i,ty,l,ofs,id,fList,tr,H1,H2. Q a l ofs tr H1 → Q ???? (eval_Efield_union ge e m a i ty l ofs id fList tr H1 H2))
  (a:expr) (loc:block) (ofs:offset) (tr:trace) (ev:eval_lvalue ge e m a loc ofs tr) on ev : Q a loc ofs tr ev ≝
  match ev with
  [ eval_Evar_local id l ty H ⇒ lvl id l ty H
  | eval_Evar_global id l ty H1 H2 ⇒ lvg id l ty H1 H2
  | eval_Ederef a ty r l pc ofs tr H ⇒ lde a ty r l pc ofs tr H (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a (Vptr (mk_pointer r l pc ofs)) tr H)
  | eval_Efield_struct a i ty l ofs id fList delta tr H1 H2 H3 ⇒ lfs a i ty l ofs id fList delta tr H1 H2 H3 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a l ofs tr H1)
  | eval_Efield_union a i ty l ofs id fList tr H1 H2 ⇒ lfu a i ty l ofs id fList tr H1 H2 (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a l ofs tr H1)
  ].

definition combined_expr_lvalue_ind ≝
λge,e,m,P,Q,eci,ecF,elv,ead,esz,eun,ebi,ect,ecf,eo1,eo2,ea1,ea2,ecs,eco,lvl,lvg,lde,lfs,lfu.  
conj ??
  (eval_expr_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu)
  (eval_lvalue_ind2 ge e m P Q eci ecF elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu).

(* * [eval_lvalue ge e m a b ofs] defines the evaluation of expression [a]
  in l-value position.  The result is the memory location [b, ofs]
  that contains the value of the expression [a]. *)

(*
Scheme eval_expr_ind22 := Minimality for eval_expr Sort Prop
  with eval_lvalue_ind2 := Minimality for eval_lvalue Sort Prop.
*)

(* * [eval_exprlist ge e m al vl] evaluates a list of r-value
  expressions [al] to their values [vl]. *)

inductive eval_exprlist (ge:genv) (e:env) (m:mem) : list expr → list val → trace → Prop ≝
  | eval_Enil:
      eval_exprlist ge e m (nil ?) (nil ?) E0
  | eval_Econs:   ∀a,bl,v,vl,tr1,tr2.
      eval_expr ge e m a v tr1 →
      eval_exprlist ge e m bl vl tr2 →
      eval_exprlist ge e m (a :: bl) (v :: vl) (tr1⧺tr2).

(*End EXPR.*)

(* * ** Transition semantics for statements and functions *)

(* * Continuations *)

inductive cont: Type[0] :=
  | Kstop: cont
  | Kseq: statement -> cont -> cont
       (**r [Kseq s2 k] = after [s1] in [s1;s2] *)
  | Kwhile: expr -> statement -> cont -> cont
       (**r [Kwhile e s k] = after [s] in [while (e) s] *)
  | Kdowhile: expr -> statement -> cont -> cont
       (**r [Kdowhile e s k] = after [s] in [do s while (e)] *)
  | Kfor2: expr -> statement -> statement -> cont -> cont
       (**r [Kfor2 e2 e3 s k] = after [s] in [for(e1;e2;e3) s] *)
  | Kfor3: expr -> statement -> statement -> cont -> cont
       (**r [Kfor3 e2 e3 s k] = after [e3] in [for(e1;e2;e3) s] *)
  | Kswitch: cont -> cont
       (**r catches [break] statements arising out of [switch] *)
  | Kcall: option (block × offset × type) -> (**r where to store result *)
           function ->                       (**r calling function *)
           env ->                            (**r local env of calling function *)
           cont -> cont.

(* * Pop continuation until a call or stop *)

let rec call_cont (k: cont) : cont :=
  match k with
  [ Kseq s k => call_cont k
  | Kwhile e s k => call_cont k
  | Kdowhile e s k => call_cont k
  | Kfor2 e2 e3 s k => call_cont k
  | Kfor3 e2 e3 s k => call_cont k
  | Kswitch k => call_cont k
  | _ => k
  ].

definition is_call_cont : cont → Prop ≝ λk.
  match k with
  [ Kstop => True
  | Kcall _ _ _ _ => True
  | _ => False
  ].

(* * States *)

inductive state: Type[0] :=
  | State:
      ∀f: function.
      ∀s: statement.
      ∀k: cont.
      ∀e: env.
      ∀m: mem.  state
  | Callstate:
      ∀fd: clight_fundef.
      ∀args: list val.
      ∀k: cont.
      ∀m: mem. state
  | Returnstate:
      ∀res: val.
      ∀k: cont.
      ∀m: mem. state.
                 
(* * Find the statement and manufacture the continuation 
  corresponding to a label *)

let rec find_label (lbl: label) (s: statement) (k: cont) 
                    on s: option (statement × cont) :=
  match s with
  [ Ssequence s1 s2 =>
      match find_label lbl s1 (Kseq s2 k) with
      [ Some sk => Some ? sk
      | None => find_label lbl s2 k
      ]
  | Sifthenelse a s1 s2 =>
      match find_label lbl s1 k with
      [ Some sk => Some ? sk
      | None => find_label lbl s2 k
      ]
  | Swhile a s1 =>
      find_label lbl s1 (Kwhile a s1 k)
  | Sdowhile a s1 =>
      find_label lbl s1 (Kdowhile a s1 k)
  | Sfor a1 a2 a3 s1 =>
      match find_label lbl a1 (Kseq (Sfor Sskip a2 a3 s1) k) with
      [ Some sk => Some ? sk
      | None =>
          match find_label lbl s1 (Kfor2 a2 a3 s1 k) with
          [ Some sk => Some ? sk
          | None => find_label lbl a3 (Kfor3 a2 a3 s1 k)
          ]
      ]
  | Sswitch e sl =>
      find_label_ls lbl sl (Kswitch k)
  | Slabel lbl' s' =>
      match ident_eq lbl lbl' with
      [ inl _ ⇒ Some ? 〈s', k〉
      | inr _ ⇒ find_label lbl s' k
      ]
  | _ => None ?
  ]

and find_label_ls (lbl: label) (sl: labeled_statements) (k: cont) 
                    on sl: option (statement × cont) :=
  match sl with
  [ LSdefault s => find_label lbl s k
  | LScase _ _ s sl' =>
      match find_label lbl s (Kseq (seq_of_labeled_statement sl') k) with
      [ Some sk => Some ? sk
      | None => find_label_ls lbl sl' k
      ]
  ].

(* * Transition relation *)

(* Strip off outer pointer for use when comparing function types. *)
definition fun_typeof ≝
λe. match typeof e with
[ Tvoid ⇒ Tvoid
| Tint a b ⇒ Tint a b
| Tfloat a ⇒ Tfloat a
| Tpointer _ ty ⇒ ty
| Tarray a b c ⇒ Tarray a b c
| Tfunction a b ⇒ Tfunction a b
| Tstruct a b ⇒ Tstruct a b
| Tunion a b ⇒ Tunion a b
| Tcomp_ptr a b ⇒ Tcomp_ptr a b
].

(* XXX: note that cost labels in exprs expose a particular eval order. *)

inductive step (ge:genv) : state → trace → state → Prop ≝

  | step_assign:   ∀f,a1,a2,k,e,m,loc,ofs,v2,m',tr1,tr2.
      eval_lvalue ge e m a1 loc ofs tr1 →
      eval_expr ge e m a2 v2 tr2 →
      store_value_of_type (typeof a1) m loc ofs v2 = Some ? m' →
      step ge (State f (Sassign a1 a2) k e m)
           (tr1⧺tr2) (State f Sskip k e m')

  | step_call_none:   ∀f,a,al,k,e,m,vf,vargs,fd,tr1,tr2.
      eval_expr ge e m a vf tr1 →
      eval_exprlist ge e m al vargs tr2 →
      find_funct ?? ge vf = Some ? fd →
      type_of_fundef fd = fun_typeof a →
      step ge (State f (Scall (None ?) a al) k e m)
           (tr1⧺tr2) (Callstate fd vargs (Kcall (None ?) f e k) m)

  | step_call_some:   ∀f,lhs,a,al,k,e,m,loc,ofs,vf,vargs,fd,tr1,tr2,tr3.
      eval_lvalue ge e m lhs loc ofs tr1 →
      eval_expr ge e m a vf tr2 →
      eval_exprlist ge e m al vargs tr3 →
      find_funct ?? ge vf = Some ? fd →
      type_of_fundef fd = fun_typeof a →
      step ge (State f (Scall (Some ? lhs) a al) k e m)
           (tr1⧺tr2⧺tr3) (Callstate fd vargs (Kcall (Some ? 〈〈loc, ofs〉, typeof lhs〉) f e k) m)

  | step_seq:  ∀f,s1,s2,k,e,m.
      step ge (State f (Ssequence s1 s2) k e m)
           E0 (State f s1 (Kseq s2 k) e m)
  | step_skip_seq: ∀f,s,k,e,m.
      step ge (State f Sskip (Kseq s k) e m)
           E0 (State f s k e m)
  | step_continue_seq: ∀f,s,k,e,m.
      step ge (State f Scontinue (Kseq s k) e m)
           E0 (State f Scontinue k e m)
  | step_break_seq: ∀f,s,k,e,m.
      step ge (State f Sbreak (Kseq s k) e m)
           E0 (State f Sbreak k e m)

  | step_ifthenelse_true:  ∀f,a,s1,s2,k,e,m,v1,tr.
      eval_expr ge e m a v1 tr →
      is_true v1 (typeof a) →
      step ge (State f (Sifthenelse a s1 s2) k e m)
           tr (State f s1 k e m)
  | step_ifthenelse_false: ∀f,a,s1,s2,k,e,m,v1,tr.
      eval_expr ge e m a v1 tr →
      is_false v1 (typeof a) →
      step ge (State f (Sifthenelse a s1 s2) k e m)
           tr (State f s2 k e m)

  | step_while_false: ∀f,a,s,k,e,m,v,tr.
      eval_expr ge e m a v tr →
      is_false v (typeof a) →
      step ge (State f (Swhile a s) k e m)
           tr (State f Sskip k e m)
  | step_while_true: ∀f,a,s,k,e,m,v,tr.
      eval_expr ge e m a v tr →
      is_true v (typeof a) →
      step ge (State f (Swhile a s) k e m)
           tr (State f s (Kwhile a s k) e m)
  | step_skip_or_continue_while: ∀f,x,a,s,k,e,m.
      x = Sskip ∨ x = Scontinue →
      step ge (State f x (Kwhile a s k) e m)
           E0 (State f (Swhile a s) k e m)
  | step_break_while: ∀f,a,s,k,e,m.
      step ge (State f Sbreak (Kwhile a s k) e m)
           E0 (State f Sskip k e m)

  | step_dowhile: ∀f,a,s,k,e,m.
      step ge (State f (Sdowhile a s) k e m)
        E0 (State f s (Kdowhile a s k) e m)
  | step_skip_or_continue_dowhile_false: ∀f,x,a,s,k,e,m,v,tr.
      x = Sskip ∨ x = Scontinue →
      eval_expr ge e m a v tr →
      is_false v (typeof a) →
      step ge (State f x (Kdowhile a s k) e m)
           tr (State f Sskip k e m)
  | step_skip_or_continue_dowhile_true: ∀f,x,a,s,k,e,m,v,tr.
      x = Sskip ∨ x = Scontinue →
      eval_expr ge e m a v tr →
      is_true v (typeof a) →
      step ge (State f x (Kdowhile a s k) e m)
           tr (State f (Sdowhile a s) k e m)
  | step_break_dowhile: ∀f,a,s,k,e,m.
      step ge (State f Sbreak (Kdowhile a s k) e m)
           E0 (State f Sskip k e m)

  | step_for_start: ∀f,a1,a2,a3,s,k,e,m.
      a1 ≠ Sskip →
      step ge (State f (Sfor a1 a2 a3 s) k e m)
           E0 (State f a1 (Kseq (Sfor Sskip a2 a3 s) k) e m)
  | step_for_false: ∀f,a2,a3,s,k,e,m,v,tr.
      eval_expr ge e m a2 v tr →
      is_false v (typeof a2) →
      step ge (State f (Sfor Sskip a2 a3 s) k e m)
           tr (State f Sskip k e m)
  | step_for_true: ∀f,a2,a3,s,k,e,m,v,tr.
      eval_expr ge e m a2 v tr →
      is_true v (typeof a2) →
      step ge (State f (Sfor Sskip a2 a3 s) k e m)
           tr (State f s (Kfor2 a2 a3 s k) e m)
  | step_skip_or_continue_for2: ∀f,x,a2,a3,s,k,e,m.
      x = Sskip ∨ x = Scontinue →
      step ge (State f x (Kfor2 a2 a3 s k) e m)
           E0 (State f a3 (Kfor3 a2 a3 s k) e m)
  | step_break_for2: ∀f,a2,a3,s,k,e,m.
      step ge (State f Sbreak (Kfor2 a2 a3 s k) e m)
           E0 (State f Sskip k e m)
  | step_skip_for3: ∀f,a2,a3,s,k,e,m.
      step ge (State f Sskip (Kfor3 a2 a3 s k) e m)
           E0 (State f (Sfor Sskip a2 a3 s) k e m)

  | step_return_0: ∀f,k,e,m.
      fn_return f = Tvoid →
      step ge (State f (Sreturn (None ?)) k e m)
           E0 (Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e)))
  | step_return_1: ∀f,a,k,e,m,v,tr.
      fn_return f ≠ Tvoid →
      eval_expr ge e m a v tr →
      step ge (State f (Sreturn (Some ? a)) k e m)
           tr (Returnstate v (call_cont k) (free_list m (blocks_of_env e)))
  | step_skip_call: ∀f,k,e,m.
      is_call_cont k →
      fn_return f = Tvoid →
      step ge (State f Sskip k e m)
           E0 (Returnstate Vundef k (free_list m (blocks_of_env e)))

  | step_switch: ∀f,a,sl,k,e,m,sz,n,tr.
      eval_expr ge e m a (Vint sz n) tr →
      step ge (State f (Sswitch a sl) k e m)
           tr (State f (seq_of_labeled_statement (select_switch ? n sl)) (Kswitch k) e m)
  | step_skip_break_switch: ∀f,x,k,e,m.
      x = Sskip ∨ x = Sbreak →
      step ge (State f x (Kswitch k) e m)
           E0 (State f Sskip k e m)
  | step_continue_switch: ∀f,k,e,m.
      step ge (State f Scontinue (Kswitch k) e m)
           E0 (State f Scontinue k e m)

  | step_label: ∀f,lbl,s,k,e,m.
      step ge (State f (Slabel lbl s) k e m)
           E0 (State f s k e m)

  | step_goto: ∀f,lbl,k,e,m,s',k'.
      find_label lbl (fn_body f) (call_cont k) = Some ? 〈s', k'〉 →
      step ge (State f (Sgoto lbl) k e m)
           E0 (State f s' k' e m)

  | step_internal_function: ∀f,vargs,k,m,e,m1,m2.
      alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) e m1 →
      bind_parameters e m1 (fn_params f) vargs m2 →
      step ge (Callstate (CL_Internal f) vargs k m)
           E0 (State f (fn_body f) k e m2)

  | step_external_function: ∀id,targs,tres,vargs,k,m,vres,t.
      event_match (external_function id targs tres) vargs t vres →
      step ge (Callstate (CL_External id targs tres) vargs k m)
            t (Returnstate vres k m)

  | step_returnstate_0: ∀v,f,e,k,m.
      step ge (Returnstate v (Kcall (None ?) f e k) m)
           E0 (State f Sskip k e m)

  | step_returnstate_1: ∀v,f,e,k,m,m',loc,ofs,ty.
      store_value_of_type ty m loc ofs v = Some ? m' →
      step ge (Returnstate v (Kcall (Some ? 〈〈loc, ofs〉, ty〉) f e k) m)
           E0 (State f Sskip k e m')
           
  | step_cost: ∀f,lbl,s,k,e,m.
      step ge (State f (Scost lbl s) k e m)
           (Echarge lbl) (State f s k e m).

(*
End SEMANTICS.
*)

(* * * Whole-program semantics *)

(* * Execution of whole programs are described as sequences of transitions
  from an initial state to a final state.  An initial state is a [Callstate]
  corresponding to the invocation of the ``main'' function of the program
  without arguments and with an empty continuation. *)

inductive initial_state (p: clight_program): state -> Prop :=
  | initial_state_intro: ∀b,f,ge,m0.
      globalenv Genv ?? (fst ??) p = ge →
      init_mem Genv ?? (fst ??) p = OK ? m0 →
      find_symbol ?? ge (prog_main ?? p) = Some ? b →
      find_funct_ptr ?? ge b = Some ? f →
      initial_state p (Callstate f (nil ?) Kstop m0).

(* * A final state is a [Returnstate] with an empty continuation. *)

inductive final_state: state -> int -> Prop :=
  | final_state_intro: ∀r,m.
      final_state (Returnstate (Vint I32 r) Kstop m) r.

(* * Execution of a whole program: [exec_program p beh]
  holds if the application of [p]'s main function to no arguments
  in the initial memory state for [p] has [beh] as observable
  behavior. *)

definition exec_program : clight_program → program_behavior → Prop ≝ λp,beh.
  ∀ge. globalenv ??? (fst ??) p = ge →
  program_behaves (mk_transrel ?? step) (initial_state p) final_state ge beh.