Changeset 2588 for src/Clight/Csem.ma


Ignore:
Timestamp:
Jan 23, 2013, 2:38:06 PM (7 years ago)
Author:
garnier
Message:

modified Cexec/Csem? semantics:
. force andbool and orbool types to be Tint sz sg, fail otherwise
. cast result of evaluation to (bitvector sz)
. in lvalue evaluation, field offset for structs is now 16 bit instead of 32
/!\ induction principles modified accordingly
. soundness and correctness adapted

modified label/labelSimulation:
. andbool and orbool are modified so that the true/false constants are

casted to the (integer) type of the enclosing expression, to match
Csem/Cexec?. If the type is not an integer, default on 32 bits.

. labelSimulation proof adapted to match changes.

proof of simulation for expressions Cl to Cm finished
. caveat : eats up all my RAM (8gb) when using matita (not matitac), barely typecheckable
. moved some lemmas from toCminorCorrectness.ma to new file toCminorOps.ma

and frontend_misc.ma to alleviate this, to no avail - more radical splitting required ?

slight modification in SimplifyCasts? to take into account modifications in semantics,
removed some duplicate lemmas and replaced them by wrappers to avoid breaking the
rest of the development.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Csem.ma

    r2569 r2588  
    129129].
    130130
    131 let rec sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
     131(* Ilias, 16 jan 2013: semantics of pointer/pointer subtraction slightly changed. Matched in toCminor.ma.
     132 * operation done on 32 bits and cast down to the target size using sign_ext or zero_ext, according to the
     133 * sign of the target type. We have to do the same in toCminor.ma
     134 * At least two things are ugly here : the fact that offsets are 32 bits (our arch is 8 bit right ?), and the downcast.
     135 * TODO: check the C standard to see if the following alternative is meaningful ?
     136 *   . the division can directly take as an argument a target size. There is also two [repr], one
     137 *     with type nat → bvint I32 (used here), one with type ∀sz. nat → bvint sz. Matching changes
     138 *     would have to be done in Cminor.
     139 *)
     140let rec sem_sub (v1:val) (t1:type) (v2: val) (t2:type) (target:type) : option val ≝
    132141  match classify_sub t1 t2 with
    133142  [ sub_case_ii _ _ ⇒                (**r integer subtraction *)
     
    149158  | sub_case_pp _ _ ty _ ⇒             (**r pointer minus pointer *)
    150159      match v1 with
    151       [ Vptr ptr1 ⇒ match v2 with
     160      [ Vptr ptr1 ⇒
     161        match v2 with
    152162        [ Vptr ptr2 ⇒
    153163          if eq_block (pblock ptr1) (pblock ptr2) then
    154164            if eqb (sizeof ty) 0 then None ?
    155             else match division_u ? (sub_offset ? (poff ptr1) (poff ptr2)) (repr (sizeof ty)) with
    156                  [ None ⇒ None ?
    157                  | Some v ⇒ Some ? (Vint I32 v) (* XXX choose size from result type? *)
    158                  ]
     165            else match target with
     166                 [ Tint tsz tsg ⇒
     167                   match division_u ? (sub_offset ? (poff ptr1) (poff ptr2)) (repr (sizeof ty)) with
     168                   [ None ⇒ None ?
     169                   | Some v ⇒
     170                     Some ? (Vint tsz (zero_ext ?? v))
     171                     (*Some ? (Vint tsz v)  XXX choose size from result type? *)
     172                   ]
     173                 | _ ⇒ None ? ]
    159174          else None ?
    160175        | _ ⇒ None ? ]
    161       | Vnull ⇒ match v2 with [ Vnull ⇒ Some ? (Vint I32 (*XXX*) (zero ?)) | _ ⇒ None ? ]
     176      | Vnull ⇒
     177        match v2 with
     178        [ Vnull ⇒
     179          match target with
     180          [ Tint tsz tsg ⇒
     181            Some ? (Vint tsz (*XXX*) (zero ?))
     182          | _ ⇒ None ? ]
     183        | _ ⇒ None ? ]
    162184      | _ ⇒ None ? ]
    163185  | sub_default _ _ ⇒ None ?
    164186  ].
     187
    165188
    166189let rec sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
     
    175198  | aop_default _ _ ⇒
    176199      None ?
    177 ].
     200  ].
    178201
    179202let rec sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val ≝
     
    285308  | _   ⇒ None ?
    286309  ].
    287  
     310
    288311let rec sem_cmp (c:comparison)
    289312                  (v1: val) (t1: type) (v2: val) (t2: type)
     
    327350  ].
    328351
     352definition cast_bool_to_target : type → option val → option val ≝
     353  λty,optv.
     354  match optv with
     355  [ None ⇒ None ?
     356  | Some v ⇒
     357    match ty with
     358    [ Tint sz sg ⇒
     359        Some ? (zero_ext sz v)
     360    | _ ⇒ None ? ]
     361  ].
     362
     363lemma cast_bool_to_target_inversion : ∀ty,v,vres.
     364  cast_bool_to_target ty (Some ? v) = Some ? vres →
     365  ∃sz,sg. ty = Tint sz sg ∧ vres = zero_ext sz v.
     366#ty #v #vres
     367cases ty
     368[ | #sz #sg | #ptr_ty | #array_ty #array_sz | #domain #codomain | #structname #fieldspec | #unionname #fieldspec | #id ]
     369whd in ⊢ ((??%%) → ?);
     370#Heq destruct
     371%{sz} %{sg} @conj try @refl
     372qed.
     373
    329374definition sem_unary_operation
    330375            : unary_operation → val → type → option val ≝
     
    339384    (op: binary_operation)
    340385    (v1: val) (t1: type) (v2: val) (t2:type)
    341     (m: mem): option val ≝
     386    (m: mem)
     387    (ty: type): option val ≝
    342388  match op with
    343389  [ Oadd ⇒ sem_add v1 t1 v2 t2
    344   | Osub ⇒ sem_sub v1 t1 v2 t2
     390  | Osub ⇒ sem_sub v1 t1 v2 t2 ty
    345391  | Omul ⇒ sem_mul v1 t1 v2 t2
    346392  | Omod ⇒ sem_mod v1 t1 v2 t2
     
    351397  | Oshl ⇒ sem_shl v1 v2
    352398  | Oshr ⇒ sem_shr v1 t1 v2 t2
    353   | Oeq ⇒ sem_cmp Ceq v1 t1 v2 t2 m
    354   | One ⇒ sem_cmp Cne v1 t1 v2 t2 m
    355   | Olt ⇒ sem_cmp Clt v1 t1 v2 t2 m
    356   | Ogt ⇒ sem_cmp Cgt v1 t1 v2 t2 m
    357   | Ole ⇒ sem_cmp Cle v1 t1 v2 t2 m
    358   | Oge ⇒ sem_cmp Cge v1 t1 v2 t2 m
     399  | Oeq ⇒ cast_bool_to_target ty (sem_cmp Ceq v1 t1 v2 t2 m)
     400  | One ⇒ cast_bool_to_target ty (sem_cmp Cne v1 t1 v2 t2 m)
     401  | Olt ⇒ cast_bool_to_target ty (sem_cmp Clt v1 t1 v2 t2 m)
     402  | Ogt ⇒ cast_bool_to_target ty (sem_cmp Cgt v1 t1 v2 t2 m)
     403  | Ole ⇒ cast_bool_to_target ty (sem_cmp Cle v1 t1 v2 t2 m)
     404  | Oge ⇒ cast_bool_to_target ty (sem_cmp Cge v1 t1 v2 t2 m)
    359405  ].
    360406
     
    554600      eval_expr ge e m a1 v1 tr1 →
    555601      eval_expr ge e m a2 v2 tr2 →
    556       sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m = Some ? v →
     602      sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m ty = Some ? v →
    557603      eval_expr ge e m (Expr (Ebinop op a1 a2) ty) v (tr1⧺tr2)
    558604  | eval_Econdition_true: ∀a1,a2,a3,ty,v1,v2,tr1,tr2.
     
    566612      eval_expr ge e m a3 v3 tr2 →
    567613      eval_expr ge e m (Expr (Econdition a1 a2 a3) ty) v3 (tr1⧺tr2)
    568   | eval_Eorbool_1: ∀a1,a2,ty,v1,tr.
     614  | eval_Eorbool_1: ∀a1,a2,ty,v1,tr,vres.
    569615      eval_expr ge e m a1 v1 tr →
    570616      is_true v1 (typeof a1) →
    571       eval_expr ge e m (Expr (Eorbool a1 a2) ty) Vtrue tr
    572   | eval_Eorbool_2: ∀a1,a2,ty,v1,v2,v,tr1,tr2.
     617      cast_bool_to_target ty (Some ? Vtrue) = Some ? vres →
     618      eval_expr ge e m (Expr (Eorbool a1 a2) ty) vres tr
     619  | eval_Eorbool_2: ∀a1,a2,ty,v1,v2,v,tr1,tr2,vres.
    573620      eval_expr ge e m a1 v1 tr1 →
    574621      is_false v1 (typeof a1) →
    575622      eval_expr ge e m a2 v2 tr2 →
    576623      bool_of_val v2 (typeof a2) v →
    577       eval_expr ge e m (Expr (Eorbool a1 a2) ty) v (tr1⧺tr2)
    578   | eval_Eandbool_1: ∀a1,a2,ty,v1,tr.
     624      cast_bool_to_target ty (Some ? v) = Some ? vres →     
     625      eval_expr ge e m (Expr (Eorbool a1 a2) ty) vres (tr1⧺tr2)
     626  | eval_Eandbool_1: ∀a1,a2,ty,v1,tr,vres.
    579627      eval_expr ge e m a1 v1 tr →
    580628      is_false v1 (typeof a1) →
    581       eval_expr ge e m (Expr (Eandbool a1 a2) ty) Vfalse tr
    582   | eval_Eandbool_2: ∀a1,a2,ty,v1,v2,v,tr1,tr2.
     629      cast_bool_to_target ty (Some ? Vfalse) = Some ? vres →           
     630      eval_expr ge e m (Expr (Eandbool a1 a2) ty) vres tr
     631  | eval_Eandbool_2: ∀a1,a2,ty,v1,v2,v,tr1,tr2,vres.
    583632      eval_expr ge e m a1 v1 tr1 →
    584633      is_true v1 (typeof a1) →
    585634      eval_expr ge e m a2 v2 tr2 →
    586635      bool_of_val v2 (typeof a2) v →
    587       eval_expr ge e m (Expr (Eandbool a1 a2) ty) v (tr1⧺tr2)
     636      cast_bool_to_target ty (Some ? v) = Some ? vres →                 
     637      eval_expr ge e m (Expr (Eandbool a1 a2) ty) vres (tr1⧺tr2)
    588638  | eval_Ecast:   ∀a,ty,ty',v1,v,tr.
    589639      eval_expr ge e m a v1 tr →
     
    616666      eval_lvalue ge e m a l ofs tr →
    617667      typeof a = Tstruct id fList →
    618       field_offset i fList = OK ? delta →
    619       eval_lvalue ge e m (Expr (Efield a i) ty) l (shift_offset ? ofs (repr I32 delta)) tr
     668      field_offset i fList = OK ? delta → 
     669      eval_lvalue ge e m (Expr (Efield a i) ty) l (shift_offset ? ofs (repr I16 delta)) tr
    620670 | eval_Efield_union:   ∀a,i,ty,l,ofs,id,fList,tr.
    621671      eval_lvalue ge e m a l ofs tr →
     
    634684  (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))
    635685  (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))
    636   (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))
    637   (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))
    638   (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))
    639   (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))
     686  (eo1:∀a1,a2,ty,v1,tr,vres,H1,H2,H3. P a1 v1 tr H1 → P ??? (eval_Eorbool_1 ge e m a1 a2 ty v1 tr vres H1 H2 H3))
     687  (eo2:∀a1,a2,ty,v1,v2,v,tr1,tr2,vres,H1,H2,H3,H4,H5. 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 vres H1 H2 H3 H4 H5))
     688  (ea1:∀a1,a2,ty,v1,tr,vres,H1,H2,H3. P a1 v1 tr H1 → P ??? (eval_Eandbool_1 ge e m a1 a2 ty v1 tr vres H1 H2 H3))
     689  (ea2:∀a1,a2,ty,v1,v2,v,tr1,tr2,vres,H1,H2,H3,H4,H5. 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 vres H1 H2 H3 H4 H5))
    640690  (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))
    641691  (eco:∀a,ty,v,l,tr,H. P a v tr H → P ??? (eval_Ecost ge e m a ty v l tr H))
     
    651701  | 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 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H3)
    652702  | 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 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a3 v3 tr2 H3)
    653   | 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr H1)
    654   | 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 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H3)
    655   | 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr H1)
    656   | 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 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H3)
     703  | eval_Eorbool_1 a1 a2 ty v1 tr vres H1 H2 H3 ⇒ eo1 a1 a2 ty v1 tr vres H1 H2 H3 (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr H1)
     704  | eval_Eorbool_2 a1 a2 ty v1 v2 v tr1 tr2 vres H1 H2 H3 H4 H5 ⇒ eo2 a1 a2 ty v1 v2 v tr1 tr2 vres H1 H2 H3 H4 H5 (eval_expr_ind ge e m P eci 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H3)
     705  | eval_Eandbool_1 a1 a2 ty v1 tr vres H1 H2 H3 ⇒ ea1 a1 a2 ty v1 tr vres H1 H2 H3 (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a1 v1 tr H1)
     706  | eval_Eandbool_2 a1 a2 ty v1 v2 v tr1 tr2 vres H1 H2 H3 H4 H5 ⇒ ea2 a1 a2 ty v1 v2 v tr1 tr2 vres H1 H2 H3 H4 H5 (eval_expr_ind ge e m P eci 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a2 v2 tr2 H3)
    657707  | 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v1 tr H1)
    658708  | eval_Ecost a ty v l tr H ⇒ eco a ty v l tr H (eval_expr_ind ge e m P eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco a v tr H)
     
    730780] qed.
    731781*)
     782
    732783let rec eval_expr_ind2 (ge:genv) (e:env) (m:mem)
    733784  (P:∀a,v,tr. eval_expr ge e m a v tr → Prop)
     
    741792  (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))
    742793  (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))
    743   (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))
    744   (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))
    745   (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))
    746   (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))
     794  (eo1:∀a1,a2,ty,v1,tr,vres,H1,H2,H3. P a1 v1 tr H1 → P ??? (eval_Eorbool_1 ge e m a1 a2 ty v1 tr vres H1 H2 H3))
     795  (eo2:∀a1,a2,ty,v1,v2,v,tr1,tr2,vres,H1,H2,H3,H4,H5. 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 vres H1 H2 H3 H4 H5))
     796  (ea1:∀a1,a2,ty,v1,tr,vres,H1,H2,H3. P a1 v1 tr H1 → P ??? (eval_Eandbool_1 ge e m a1 a2 ty v1 tr vres H1 H2 H3))
     797  (ea2:∀a1,a2,ty,v1,v2,v,tr1,tr2,vres,H1,H2,H3,H4,H5. 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 vres H1 H2 H3 H4 H5))
    747798  (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))
    748799  (eco:∀a,ty,v,l,tr,H. P a v tr H → P ??? (eval_Ecost ge e m a ty v l tr H))
     
    763814  | 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 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H3)
    764815  | 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 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a3 v3 tr2 H3)
    765   | 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr H1)
    766   | 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 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H3)
    767   | 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr H1)
    768   | 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 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H3)
     816  | eval_Eorbool_1 a1 a2 ty v1 tr vres H1 H2 H3 ⇒ eo1 a1 a2 ty v1 tr vres H1 H2 H3 (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr H1)
     817  | eval_Eorbool_2 a1 a2 ty v1 v2 v tr1 tr2 vres H1 H2 H3 H4 H5 ⇒ eo2 a1 a2 ty v1 v2 v tr1 tr2 vres H1 H2 H3 H4 H5 (eval_expr_ind2 ge e m P Q eci 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H3)
     818  | eval_Eandbool_1 a1 a2 ty v1 tr vres H1 H2 H3 ⇒ ea1 a1 a2 ty v1 tr vres H1 H2 H3 (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a1 v1 tr H1)
     819  | eval_Eandbool_2 a1 a2 ty v1 v2 v tr1 tr2 vres H1 H2 H3 H4 H5 ⇒ ea2 a1 a2 ty v1 v2 v tr1 tr2 vres H1 H2 H3 H4 H5 (eval_expr_ind2 ge e m P Q eci 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a2 v2 tr2 H3)
    769820  | 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 elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a v1 tr H1)
    770821  | eval_Ecost a ty v l tr H ⇒ eco a ty v l tr H (eval_expr_ind2 ge e m P Q eci elv ead esz eun ebi ect ecf eo1 eo2 ea1 ea2 ecs eco lvl lvg lde lfs lfu a v tr H)
     
    781832  (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))
    782833  (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))
    783   (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))
    784   (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))
    785   (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))
    786   (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))
     834  (eo1:∀a1,a2,ty,v1,tr,vres,H1,H2,H3. P a1 v1 tr H1 → P ??? (eval_Eorbool_1 ge e m a1 a2 ty v1 tr vres H1 H2 H3))
     835  (eo2:∀a1,a2,ty,v1,v2,v,tr1,tr2,vres,H1,H2,H3,H4,H5. 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 vres H1 H2 H3 H4 H5))
     836  (ea1:∀a1,a2,ty,v1,tr,vres,H1,H2,H3. P a1 v1 tr H1 → P ??? (eval_Eandbool_1 ge e m a1 a2 ty v1 tr vres H1 H2 H3))
     837  (ea2:∀a1,a2,ty,v1,v2,v,tr1,tr2,vres,H1,H2,H3,H4,H5. 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 vres H1 H2 H3 H4 H5))
    787838  (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))
    788839  (eco:∀a,ty,v,l,tr,H. P a v tr H → P ??? (eval_Ecost ge e m a ty v l tr H))
Note: See TracChangeset for help on using the changeset viewer.